WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 420 ms] (2) CpxRelTRS (3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxRelTRS (5) SlicingProof [LOWER BOUND(ID), 0 ms] (6) CpxRelTRS (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) typed CpxTrs (9) OrderProof [LOWER BOUND(ID), 0 ms] (10) typed CpxTrs (11) RewriteLemmaProof [LOWER BOUND(ID), 309 ms] (12) typed CpxTrs (13) RewriteLemmaProof [LOWER BOUND(ID), 1523 ms] (14) BEST (15) proven lower bound (16) LowerBoundPropagationProof [FINISHED, 0 ms] (17) BOUNDS(n^1, INF) (18) typed CpxTrs (19) RewriteLemmaProof [LOWER BOUND(ID), 231 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 2394 ms] (22) BOUNDS(1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), x, a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0, S(y)) -> False !EQ(S(x), 0) -> False !EQ(0, 0) -> True red[Let][Let](e, Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](e, App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](e, V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](App(e1, e2), f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, x, a, e) -> e subst[Ite](True, x, a, e) -> a Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), x, a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0, S(y)) -> False !EQ(S(x), 0) -> False !EQ(0, 0) -> True red[Let][Let](e, Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](e, App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](e, V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](App(e1, e2), f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, x, a, e) -> e subst[Ite](True, x, a, e) -> a Rewrite Strategy: INNERMOST ---------------------------------------- (3) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), x, a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](e, Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](e, App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](e, V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](App(e1, e2), f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, x, a, e) -> e subst[Ite](True, x, a, e) -> a Rewrite Strategy: INNERMOST ---------------------------------------- (5) SlicingProof (LOWER BOUND(ID)) Sliced the following arguments: subst[Ite]/1 red[Let][Let]/0 ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Innermost TRS: Rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Types: subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V App :: App:Lam:V -> App:Lam:V -> App:Lam:V mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V Lam :: S:0' -> App:Lam:V -> App:Lam:V subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V eqTerm :: App:Lam:V -> App:Lam:V -> False:True V :: S:0' -> App:Lam:V red :: App:Lam:V -> App:Lam:V red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V and :: False:True -> False:True -> False:True False :: False:True !EQ :: S:0' -> S:0' -> False:True mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V lamvar :: App:Lam:V -> App:Lam:V lambody :: App:Lam:V -> App:Lam:V isvar :: App:Lam:V -> False:True True :: False:True islam :: App:Lam:V -> False:True appe2 :: App:Lam:V -> App:Lam:V appe1 :: App:Lam:V -> App:Lam:V lambdaint :: App:Lam:V -> App:Lam:V S :: S:0' -> S:0' 0' :: S:0' red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V hole_App:Lam:V1_0 :: App:Lam:V hole_S:0'2_0 :: S:0' hole_False:True3_0 :: False:True gen_App:Lam:V4_0 :: Nat -> App:Lam:V gen_S:0'5_0 :: Nat -> S:0' ---------------------------------------- (9) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: subst, eqTerm, red, !EQ They will be analysed ascendingly in the following order: eqTerm < subst subst < red !EQ < eqTerm ---------------------------------------- (10) Obligation: Innermost TRS: Rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Types: subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V App :: App:Lam:V -> App:Lam:V -> App:Lam:V mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V Lam :: S:0' -> App:Lam:V -> App:Lam:V subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V eqTerm :: App:Lam:V -> App:Lam:V -> False:True V :: S:0' -> App:Lam:V red :: App:Lam:V -> App:Lam:V red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V and :: False:True -> False:True -> False:True False :: False:True !EQ :: S:0' -> S:0' -> False:True mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V lamvar :: App:Lam:V -> App:Lam:V lambody :: App:Lam:V -> App:Lam:V isvar :: App:Lam:V -> False:True True :: False:True islam :: App:Lam:V -> False:True appe2 :: App:Lam:V -> App:Lam:V appe1 :: App:Lam:V -> App:Lam:V lambdaint :: App:Lam:V -> App:Lam:V S :: S:0' -> S:0' 0' :: S:0' red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V hole_App:Lam:V1_0 :: App:Lam:V hole_S:0'2_0 :: S:0' hole_False:True3_0 :: False:True gen_App:Lam:V4_0 :: Nat -> App:Lam:V gen_S:0'5_0 :: Nat -> S:0' Generator Equations: gen_App:Lam:V4_0(0) <=> V(0') gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0')) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: !EQ, subst, eqTerm, red They will be analysed ascendingly in the following order: eqTerm < subst subst < red !EQ < eqTerm ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: !EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0) Induction Base: !EQ(gen_S:0'5_0(0), gen_S:0'5_0(+(1, 0))) ->_R^Omega(0) False Induction Step: !EQ(gen_S:0'5_0(+(n7_0, 1)), gen_S:0'5_0(+(1, +(n7_0, 1)))) ->_R^Omega(0) !EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) ->_IH False We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (12) Obligation: Innermost TRS: Rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Types: subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V App :: App:Lam:V -> App:Lam:V -> App:Lam:V mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V Lam :: S:0' -> App:Lam:V -> App:Lam:V subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V eqTerm :: App:Lam:V -> App:Lam:V -> False:True V :: S:0' -> App:Lam:V red :: App:Lam:V -> App:Lam:V red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V and :: False:True -> False:True -> False:True False :: False:True !EQ :: S:0' -> S:0' -> False:True mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V lamvar :: App:Lam:V -> App:Lam:V lambody :: App:Lam:V -> App:Lam:V isvar :: App:Lam:V -> False:True True :: False:True islam :: App:Lam:V -> False:True appe2 :: App:Lam:V -> App:Lam:V appe1 :: App:Lam:V -> App:Lam:V lambdaint :: App:Lam:V -> App:Lam:V S :: S:0' -> S:0' 0' :: S:0' red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V hole_App:Lam:V1_0 :: App:Lam:V hole_S:0'2_0 :: S:0' hole_False:True3_0 :: False:True gen_App:Lam:V4_0 :: Nat -> App:Lam:V gen_S:0'5_0 :: Nat -> S:0' Lemmas: !EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0) Generator Equations: gen_App:Lam:V4_0(0) <=> V(0') gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0')) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: eqTerm, subst, red They will be analysed ascendingly in the following order: eqTerm < subst subst < red ---------------------------------------- (13) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)) -> False, rt in Omega(1 + n460_0) Induction Base: eqTerm(gen_App:Lam:V4_0(+(1, 0)), gen_App:Lam:V4_0(0)) ->_R^Omega(1) False Induction Step: eqTerm(gen_App:Lam:V4_0(+(1, +(n460_0, 1))), gen_App:Lam:V4_0(+(n460_0, 1))) ->_R^Omega(1) and(eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)), eqTerm(V(0'), V(0'))) ->_IH and(False, eqTerm(V(0'), V(0'))) ->_R^Omega(1) and(False, !EQ(0', 0')) ->_R^Omega(0) and(False, True) ->_R^Omega(0) False We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (14) Complex Obligation (BEST) ---------------------------------------- (15) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Types: subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V App :: App:Lam:V -> App:Lam:V -> App:Lam:V mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V Lam :: S:0' -> App:Lam:V -> App:Lam:V subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V eqTerm :: App:Lam:V -> App:Lam:V -> False:True V :: S:0' -> App:Lam:V red :: App:Lam:V -> App:Lam:V red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V and :: False:True -> False:True -> False:True False :: False:True !EQ :: S:0' -> S:0' -> False:True mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V lamvar :: App:Lam:V -> App:Lam:V lambody :: App:Lam:V -> App:Lam:V isvar :: App:Lam:V -> False:True True :: False:True islam :: App:Lam:V -> False:True appe2 :: App:Lam:V -> App:Lam:V appe1 :: App:Lam:V -> App:Lam:V lambdaint :: App:Lam:V -> App:Lam:V S :: S:0' -> S:0' 0' :: S:0' red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V hole_App:Lam:V1_0 :: App:Lam:V hole_S:0'2_0 :: S:0' hole_False:True3_0 :: False:True gen_App:Lam:V4_0 :: Nat -> App:Lam:V gen_S:0'5_0 :: Nat -> S:0' Lemmas: !EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0) Generator Equations: gen_App:Lam:V4_0(0) <=> V(0') gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0')) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: eqTerm, subst, red They will be analysed ascendingly in the following order: eqTerm < subst subst < red ---------------------------------------- (16) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (17) BOUNDS(n^1, INF) ---------------------------------------- (18) Obligation: Innermost TRS: Rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Types: subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V App :: App:Lam:V -> App:Lam:V -> App:Lam:V mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V Lam :: S:0' -> App:Lam:V -> App:Lam:V subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V eqTerm :: App:Lam:V -> App:Lam:V -> False:True V :: S:0' -> App:Lam:V red :: App:Lam:V -> App:Lam:V red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V and :: False:True -> False:True -> False:True False :: False:True !EQ :: S:0' -> S:0' -> False:True mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V lamvar :: App:Lam:V -> App:Lam:V lambody :: App:Lam:V -> App:Lam:V isvar :: App:Lam:V -> False:True True :: False:True islam :: App:Lam:V -> False:True appe2 :: App:Lam:V -> App:Lam:V appe1 :: App:Lam:V -> App:Lam:V lambdaint :: App:Lam:V -> App:Lam:V S :: S:0' -> S:0' 0' :: S:0' red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V hole_App:Lam:V1_0 :: App:Lam:V hole_S:0'2_0 :: S:0' hole_False:True3_0 :: False:True gen_App:Lam:V4_0 :: Nat -> App:Lam:V gen_S:0'5_0 :: Nat -> S:0' Lemmas: !EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0) eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)) -> False, rt in Omega(1 + n460_0) Generator Equations: gen_App:Lam:V4_0(0) <=> V(0') gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0')) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: subst, red They will be analysed ascendingly in the following order: subst < red ---------------------------------------- (19) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369328_0)) -> gen_App:Lam:V4_0(n369328_0), rt in Omega(1 + n369328_0) Induction Base: subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(0)) ->_R^Omega(1) subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(b), V(0')) ->_L^Omega(1) subst[Ite](False, gen_App:Lam:V4_0(b), V(0')) ->_R^Omega(0) V(0') Induction Step: subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(+(n369328_0, 1))) ->_R^Omega(1) mkapp(subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369328_0)), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) ->_IH mkapp(gen_App:Lam:V4_0(c369329_0), subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), V(0'))) ->_R^Omega(1) mkapp(gen_App:Lam:V4_0(n369328_0), subst[Ite](eqTerm(gen_App:Lam:V4_0(1), V(0')), gen_App:Lam:V4_0(b), V(0'))) ->_L^Omega(1) mkapp(gen_App:Lam:V4_0(n369328_0), subst[Ite](False, gen_App:Lam:V4_0(b), V(0'))) ->_R^Omega(0) mkapp(gen_App:Lam:V4_0(n369328_0), V(0')) ->_R^Omega(1) App(gen_App:Lam:V4_0(n369328_0), V(0')) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (20) Obligation: Innermost TRS: Rules: subst(x, a, App(e1, e2)) -> mkapp(subst(x, a, e1), subst(x, a, e2)) subst(x, a, Lam(var, exp)) -> subst[True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) red(App(e1, e2)) -> red[Let](App(e1, e2), red(e1)) red(Lam(int, term)) -> Lam(int, term) subst(x, a, V(int)) -> subst[Ite](eqTerm(x, V(int)), a, V(int)) red(V(int)) -> V(int) eqTerm(App(t11, t12), App(t21, t22)) -> and(eqTerm(t11, t21), eqTerm(t12, t22)) eqTerm(App(t11, t12), Lam(i2, l2)) -> False eqTerm(App(t11, t12), V(v2)) -> False eqTerm(Lam(i1, l1), App(t21, t22)) -> False eqTerm(Lam(i1, l1), Lam(i2, l2)) -> and(!EQ(i1, i2), eqTerm(l1, l2)) eqTerm(Lam(i1, l1), V(v2)) -> False eqTerm(V(v1), App(t21, t22)) -> False eqTerm(V(v1), Lam(i2, l2)) -> False eqTerm(V(v1), V(v2)) -> !EQ(v1, v2) mklam(V(name), e) -> Lam(name, e) lamvar(Lam(var, exp)) -> V(var) lambody(Lam(var, exp)) -> exp isvar(App(t1, t2)) -> False isvar(Lam(int, term)) -> False isvar(V(int)) -> True islam(App(t1, t2)) -> False islam(Lam(int, term)) -> True islam(V(int)) -> False appe2(App(e1, e2)) -> e2 appe1(App(e1, e2)) -> e1 mkapp(e1, e2) -> App(e1, e2) lambdaint(e) -> red(e) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True !EQ(S(x), S(y)) -> !EQ(x, y) !EQ(0', S(y)) -> False !EQ(S(x), 0') -> False !EQ(0', 0') -> True red[Let][Let](Lam(var, exp), a) -> red(subst(V(var), a, exp)) subst[True][Ite](False, x, a, Lam(var, exp)) -> mklam(V(var), subst(x, a, exp)) red[Let][Let](App(t1, t2), e2) -> App(App(t1, t2), e2) red[Let][Let](V(int), e2) -> App(V(int), e2) red[Let](App(e1, e2), f) -> red[Let][Let](f, red(e2)) subst[True][Ite](True, x, a, e) -> e subst[Ite](False, a, e) -> e subst[Ite](True, a, e) -> a Types: subst :: App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V App :: App:Lam:V -> App:Lam:V -> App:Lam:V mkapp :: App:Lam:V -> App:Lam:V -> App:Lam:V Lam :: S:0' -> App:Lam:V -> App:Lam:V subst[True][Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V -> App:Lam:V eqTerm :: App:Lam:V -> App:Lam:V -> False:True V :: S:0' -> App:Lam:V red :: App:Lam:V -> App:Lam:V red[Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V subst[Ite] :: False:True -> App:Lam:V -> App:Lam:V -> App:Lam:V and :: False:True -> False:True -> False:True False :: False:True !EQ :: S:0' -> S:0' -> False:True mklam :: App:Lam:V -> App:Lam:V -> App:Lam:V lamvar :: App:Lam:V -> App:Lam:V lambody :: App:Lam:V -> App:Lam:V isvar :: App:Lam:V -> False:True True :: False:True islam :: App:Lam:V -> False:True appe2 :: App:Lam:V -> App:Lam:V appe1 :: App:Lam:V -> App:Lam:V lambdaint :: App:Lam:V -> App:Lam:V S :: S:0' -> S:0' 0' :: S:0' red[Let][Let] :: App:Lam:V -> App:Lam:V -> App:Lam:V hole_App:Lam:V1_0 :: App:Lam:V hole_S:0'2_0 :: S:0' hole_False:True3_0 :: False:True gen_App:Lam:V4_0 :: Nat -> App:Lam:V gen_S:0'5_0 :: Nat -> S:0' Lemmas: !EQ(gen_S:0'5_0(n7_0), gen_S:0'5_0(+(1, n7_0))) -> False, rt in Omega(0) eqTerm(gen_App:Lam:V4_0(+(1, n460_0)), gen_App:Lam:V4_0(n460_0)) -> False, rt in Omega(1 + n460_0) subst(gen_App:Lam:V4_0(1), gen_App:Lam:V4_0(b), gen_App:Lam:V4_0(n369328_0)) -> gen_App:Lam:V4_0(n369328_0), rt in Omega(1 + n369328_0) Generator Equations: gen_App:Lam:V4_0(0) <=> V(0') gen_App:Lam:V4_0(+(x, 1)) <=> App(gen_App:Lam:V4_0(x), V(0')) gen_S:0'5_0(0) <=> 0' gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x)) The following defined symbols remain to be analysed: red ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: red(gen_App:Lam:V4_0(n374311_0)) -> *6_0, rt in Omega(n374311_0) Induction Base: red(gen_App:Lam:V4_0(0)) Induction Step: red(gen_App:Lam:V4_0(+(n374311_0, 1))) ->_R^Omega(1) red[Let](App(gen_App:Lam:V4_0(n374311_0), V(0')), red(gen_App:Lam:V4_0(n374311_0))) ->_IH red[Let](App(gen_App:Lam:V4_0(n374311_0), V(0')), *6_0) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (22) BOUNDS(1, INF)