YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 TransformationProof (⇔, 0 ms)
↳27 QDP
↳28 Induction-Processor (⇒, 7 ms)
↳29 AND
↳30 QDP
↳31 DependencyGraphProof (⇔, 0 ms)
↳32 TRUE
↳33 QTRS
↳34 QTRSRRRProof (⇔, 0 ms)
↳35 QTRS
↳36 RisEmptyProof (⇔, 0 ms)
↳37 YES
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
MOD(s(x), s(y)) → LE(y, x)
IF_MOD(true, x, y) → MOD(minus(x, y), y)
IF_MOD(true, x, y) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, x, y) → MOD(minus(x, y), y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, x, y) → mod(minus(x, y), y)
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, x, y) → MOD(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, x0, x1)
if_mod(false, s(x0), s(x1))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, x, y) → MOD(minus(x, y), y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
IF_MOD(true, s(z0), s(z1)) → MOD(minus(s(z0), s(z1)), s(z1)) → IF_MOD(true, s(z0), s(z1)) → MOD(minus(s(z0), s(z1)), s(z1))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
IF_MOD(true, s(z0), s(z1)) → MOD(minus(s(z0), s(z1)), s(z1))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
POL(0) = 1
POL(IF_MOD(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(MOD(x1, x2)) = 1 + x1 + x2
POL(false_renamed) = 0
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true_renamed) = 0
proof of internal # AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished Partial correctness of the following Program [x, v18, v19, v20, x', x'', y', v11, y'', x1, x2, y1] equal_bool(true, false) -> false equal_bool(false, true) -> false equal_bool(true, true) -> true equal_bool(false, false) -> true true and x -> x false and x -> false true or x -> true false or x -> x not(false) -> true not(true) -> false isa_true(true) -> true isa_true(false) -> false isa_false(true) -> false isa_false(false) -> true equal_sort[a0](0, 0) -> true equal_sort[a0](0, s(v18)) -> false equal_sort[a0](s(v19), 0) -> false equal_sort[a0](s(v19), s(v20)) -> equal_sort[a0](v19, v20) equal_sort[a19](true_renamed, true_renamed) -> true equal_sort[a19](true_renamed, false_renamed) -> false equal_sort[a19](false_renamed, true_renamed) -> false equal_sort[a19](false_renamed, false_renamed) -> true equal_sort[a24](witness_sort[a24], witness_sort[a24]) -> true minus'(x', 0) -> false minus'(s(x''), s(y')) -> true minus'(0, s(v11)) -> false minus(x', 0) -> x' minus(s(x''), s(y')) -> minus(x'', y') minus(0, s(v11)) -> 0 le(0, y'') -> true_renamed le(s(x1), 0) -> false_renamed le(s(x2), s(y1)) -> le(x2, y1) using the following formula: z2:sort[a0],z3:sort[a0].((~(z2=0)/\~(z3=0))->minus'(z2, z3)=true) could be successfully shown: (0) Formula (1) Induction by data structure [EQUIVALENT, 0 ms] (2) AND (3) Formula (4) Symbolic evaluation [EQUIVALENT, 0 ms] (5) YES (6) Formula (7) Symbolic evaluation [EQUIVALENT, 0 ms] (8) Formula (9) Case Analysis [EQUIVALENT, 0 ms] (10) AND (11) Formula (12) Symbolic evaluation [EQUIVALENT, 0 ms] (13) YES (14) Formula (15) Symbolic evaluation [EQUIVALENT, 0 ms] (16) YES ---------------------------------------- (0) Obligation: Formula: z2:sort[a0],z3:sort[a0].((~(z2=0)/\~(z3=0))->minus'(z2, z3)=true) There are no hypotheses. ---------------------------------------- (1) Induction by data structure (EQUIVALENT) Induction by data structure sort[a0] generates the following cases: 1. Base Case: Formula: z3:sort[a0].((~(0=0)/\~(z3=0))->minus'(0, z3)=true) There are no hypotheses. 1. Step Case: Formula: n:sort[a0],z3:sort[a0].((~(s(n)=0)/\~(z3=0))->minus'(s(n), z3)=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) ---------------------------------------- (2) Complex Obligation (AND) ---------------------------------------- (3) Obligation: Formula: z3:sort[a0].((~(0=0)/\~(z3=0))->minus'(0, z3)=true) There are no hypotheses. ---------------------------------------- (4) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (5) YES ---------------------------------------- (6) Obligation: Formula: n:sort[a0],z3:sort[a0].((~(s(n)=0)/\~(z3=0))->minus'(s(n), z3)=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) ---------------------------------------- (7) Symbolic evaluation (EQUIVALENT) Could be shown by simple symbolic evaluation. ---------------------------------------- (8) Obligation: Formula: z3:sort[a0],n:sort[a0].(~(z3=0)->minus'(s(n), z3)=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) ---------------------------------------- (9) Case Analysis (EQUIVALENT) Case analysis leads to the following new obligations: Formula: n:sort[a0].(~(0=0)->minus'(s(n), 0)=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) Formula: x_1:sort[a0],n:sort[a0].(~(s(x_1)=0)->minus'(s(n), s(x_1))=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) ---------------------------------------- (10) Complex Obligation (AND) ---------------------------------------- (11) Obligation: Formula: n:sort[a0].(~(0=0)->minus'(s(n), 0)=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) ---------------------------------------- (12) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (13) YES ---------------------------------------- (14) Obligation: Formula: x_1:sort[a0],n:sort[a0].(~(s(x_1)=0)->minus'(s(n), s(x_1))=true) Hypotheses: n:sort[a0],!z3:sort[a0].((~(n=0)/\~(z3=0))->minus'(n, z3)=true) ---------------------------------------- (15) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (16) YES
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(x0, 0)
minus(s(x0), s(x1))
minus'(x', 0) → false
minus'(s(x''), s(y')) → true
minus'(0, s(v11)) → false
minus(x', 0) → x'
minus(s(x''), s(y')) → minus(x'', y')
le(0, y'') → true_renamed
le(s(x1), 0) → false_renamed
le(s(x2), s(y1)) → le(x2, y1)
minus(0, s(v11)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v18)) → false
equal_sort[a0](s(v19), 0) → false
equal_sort[a0](s(v19), s(v20)) → equal_sort[a0](v19, v20)
equal_sort[a19](true_renamed, true_renamed) → true
equal_sort[a19](true_renamed, false_renamed) → false
equal_sort[a19](false_renamed, true_renamed) → false
equal_sort[a19](false_renamed, false_renamed) → true
equal_sort[a24](witness_sort[a24], witness_sort[a24]) → true
isatrue1 > witnesssort[a24] > equalsort[a24]2 > equalsort[a19]2 > or2 > le2 > equalsort[a0]2 > not1 > isafalse1 > equalbool2 > minus2 > 0 > false > minus'2 > true > s1 > truerenamed > and2 > falserenamed
0=4
false=9
true=9
true_renamed=5
false_renamed=6
witness_sort[a24]=1
s_1=1
not_1=1
isa_true_1=0
isa_false_1=1
minus'_2=5
minus_2=0
le_2=0
equal_bool_2=0
and_2=0
or_2=0
equal_sort[a0]_2=3
equal_sort[a19]_2=0
equal_sort[a24]_2=7
minus'(x', 0) → false
minus'(s(x''), s(y')) → true
minus'(0, s(v11)) → false
minus(x', 0) → x'
minus(s(x''), s(y')) → minus(x'', y')
le(0, y'') → true_renamed
le(s(x1), 0) → false_renamed
le(s(x2), s(y1)) → le(x2, y1)
minus(0, s(v11)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v18)) → false
equal_sort[a0](s(v19), 0) → false
equal_sort[a0](s(v19), s(v20)) → equal_sort[a0](v19, v20)
equal_sort[a19](true_renamed, true_renamed) → true
equal_sort[a19](true_renamed, false_renamed) → false
equal_sort[a19](false_renamed, true_renamed) → false
equal_sort[a19](false_renamed, false_renamed) → true
equal_sort[a24](witness_sort[a24], witness_sort[a24]) → true