YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 7 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 Induction-Processor (⇒, 25 ms)
↳27 AND
↳28 QDP
↳29 PisEmptyProof (⇔, 0 ms)
↳30 YES
↳31 QTRS
↳32 QTRSRRRProof (⇔, 0 ms)
↳33 QTRS
↳34 RisEmptyProof (⇔, 0 ms)
↳35 YES
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
LEQ(s(x), s(y)) → LEQ(x, y)
-1(s(x), s(y)) → -1(x, y)
MOD(s(x), s(y)) → IF(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
MOD(s(x), s(y)) → LEQ(y, x)
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
MOD(s(x), s(y)) → -1(s(x), s(y))
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
-1(s(x), s(y)) → -1(x, y)
From the DPs we obtained the following set of size-change graphs:
LEQ(s(x), s(y)) → LEQ(x, y)
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
LEQ(s(x), s(y)) → LEQ(x, y)
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
LEQ(s(x), s(y)) → LEQ(x, y)
From the DPs we obtained the following set of size-change graphs:
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
leq(0, y) → true
leq(s(x), 0) → false
leq(s(x), s(y)) → leq(x, y)
if(true, x, y) → x
if(false, x, y) → y
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
-(x0, 0)
-(s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
leq(0, x0)
leq(s(x0), 0)
leq(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
MOD(s(x), s(y)) → MOD(-(s(x), s(y)), s(y))
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
-(x0, 0)
-(s(x0), s(x1))
POL(-(x1, x2)) = x1
POL(0) = 0
POL(MOD(x1, x2)) = x1
POL(s(x1)) = 1 + x1
proof of internal # AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished Partial correctness of the following Program [x, v5, v6, v7, x', y', x'', v4] 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](s(v5), s(v6)) -> equal_sort[a0](v5, v6) equal_sort[a0](s(v5), 0) -> false equal_sort[a0](0, s(v7)) -> false equal_sort[a0](0, 0) -> true equal_sort[a13](witness_sort[a13], witness_sort[a13]) -> true -'(s(x'), s(y')) -> true -'(x'', 0) -> false -'(0, s(v4)) -> false -(s(x'), s(y')) -> -(x', y') -(x'', 0) -> x'' -(0, s(v4)) -> 0 using the following formula: x:sort[a0],y:sort[a0].-'(s(x), s(y))=true could be successfully shown: (0) Formula (1) Symbolic evaluation [EQUIVALENT, 0 ms] (2) YES ---------------------------------------- (0) Obligation: Formula: x:sort[a0],y:sort[a0].-'(s(x), s(y))=true There are no hypotheses. ---------------------------------------- (1) Symbolic evaluation (EQUIVALENT) Could be reduced to the following new obligation by simple symbolic evaluation: True ---------------------------------------- (2) YES
-(s(x), s(y)) → -(x, y)
-(x, 0) → x
-(x0, 0)
-(s(x0), s(x1))
-'(s(x'), s(y')) → true
-'(x'', 0) → false
-'(0, s(v4)) → false
-(s(x'), s(y')) → -(x', y')
-(x'', 0) → x''
-(0, s(v4)) → 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](s(v5), s(v6)) → equal_sort[a0](v5, v6)
equal_sort[a0](s(v5), 0) → false
equal_sort[a0](0, s(v7)) → false
equal_sort[a0](0, 0) → true
equal_sort[a13](witness_sort[a13], witness_sort[a13]) → true
isatrue1 > witnesssort[a13] > equalsort[a13]2 > -'2 > equalsort[a0]2 > isafalse1 > -2 > not1 > or2 > false > true > equalbool2 > and2 > 0 > s1
true=4
0=3
false=3
witness_sort[a13]=1
s_1=1
not_1=1
isa_true_1=0
isa_false_1=2
-'_2=0
-_2=0
equal_bool_2=0
and_2=0
or_2=0
equal_sort[a0]_2=0
equal_sort[a13]_2=3
-'(s(x'), s(y')) → true
-'(x'', 0) → false
-'(0, s(v4)) → false
-(s(x'), s(y')) → -(x', y')
-(x'', 0) → x''
-(0, s(v4)) → 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](s(v5), s(v6)) → equal_sort[a0](v5, v6)
equal_sort[a0](s(v5), 0) → false
equal_sort[a0](0, s(v7)) → false
equal_sort[a0](0, 0) → true
equal_sort[a13](witness_sort[a13], witness_sort[a13]) → true