WORST_CASE(NON_POLY,?)
proof of input_n8vvm2KoA0.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 208 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 49 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 51 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 994 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [FINISHED, 587 ms]
(16) BOUNDS(EXP, INF)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   disj(T) -> True
   disj(F) -> True
   conj(Or(o1, o2)) -> False
   conj(T) -> True
   conj(F) -> True
   disj(And(a1, a2)) -> conj(And(a1, a2))
   disj(Or(t1, t2)) -> and(conj(t1), disj(t1))
   conj(And(t1, t2)) -> and(disj(t1), conj(t1))
   bool(T) -> True
   bool(F) -> True
   bool(And(a1, a2)) -> False
   bool(Or(o1, o2)) -> False
   isConsTerm(T, T) -> True
   isConsTerm(T, F) -> False
   isConsTerm(T, And(y1, y2)) -> False
   isConsTerm(T, Or(x1, x2)) -> False
   isConsTerm(F, T) -> False
   isConsTerm(F, F) -> True
   isConsTerm(F, And(y1, y2)) -> False
   isConsTerm(F, Or(x1, x2)) -> False
   isConsTerm(And(a1, a2), T) -> False
   isConsTerm(And(a1, a2), F) -> False
   isConsTerm(And(a1, a2), And(y1, y2)) -> True
   isConsTerm(And(a1, a2), Or(x1, x2)) -> False
   isConsTerm(Or(o1, o2), T) -> False
   isConsTerm(Or(o1, o2), F) -> False
   isConsTerm(Or(o1, o2), And(y1, y2)) -> False
   isConsTerm(Or(o1, o2), Or(x1, x2)) -> True
   isOp(T) -> False
   isOp(F) -> False
   isOp(And(t1, t2)) -> True
   isOp(Or(t1, t2)) -> True
   isAnd(T) -> False
   isAnd(F) -> False
   isAnd(And(t1, t2)) -> True
   isAnd(Or(t1, t2)) -> False
   getSecond(And(t1, t2)) -> t1
   getSecond(Or(t1, t2)) -> t1
   getFirst(And(t1, t2)) -> t1
   getFirst(Or(t1, t2)) -> t1
   disjconj(p) -> disj(p)

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

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   disj(T) -> True
   disj(F) -> True
   conj(Or(o1, o2)) -> False
   conj(T) -> True
   conj(F) -> True
   disj(And(a1, a2)) -> conj(And(a1, a2))
   disj(Or(t1, t2)) -> and(conj(t1), disj(t1))
   conj(And(t1, t2)) -> and(disj(t1), conj(t1))
   bool(T) -> True
   bool(F) -> True
   bool(And(a1, a2)) -> False
   bool(Or(o1, o2)) -> False
   isConsTerm(T, T) -> True
   isConsTerm(T, F) -> False
   isConsTerm(T, And(y1, y2)) -> False
   isConsTerm(T, Or(x1, x2)) -> False
   isConsTerm(F, T) -> False
   isConsTerm(F, F) -> True
   isConsTerm(F, And(y1, y2)) -> False
   isConsTerm(F, Or(x1, x2)) -> False
   isConsTerm(And(a1, a2), T) -> False
   isConsTerm(And(a1, a2), F) -> False
   isConsTerm(And(a1, a2), And(y1, y2)) -> True
   isConsTerm(And(a1, a2), Or(x1, x2)) -> False
   isConsTerm(Or(o1, o2), T) -> False
   isConsTerm(Or(o1, o2), F) -> False
   isConsTerm(Or(o1, o2), And(y1, y2)) -> False
   isConsTerm(Or(o1, o2), Or(x1, x2)) -> True
   isOp(T) -> False
   isOp(F) -> False
   isOp(And(t1, t2)) -> True
   isOp(Or(t1, t2)) -> True
   isAnd(T) -> False
   isAnd(F) -> False
   isAnd(And(t1, t2)) -> True
   isAnd(Or(t1, t2)) -> False
   getSecond(And(t1, t2)) -> t1
   getSecond(Or(t1, t2)) -> t1
   getFirst(And(t1, t2)) -> t1
   getFirst(Or(t1, t2)) -> t1
   disjconj(p) -> disj(p)

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

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   disj(T) -> True
   disj(F) -> True
   disj(And(z0, z1)) -> conj(And(z0, z1))
   disj(Or(z0, z1)) -> and(conj(z0), disj(z0))
   conj(Or(z0, z1)) -> False
   conj(T) -> True
   conj(F) -> True
   conj(And(z0, z1)) -> and(disj(z0), conj(z0))
   bool(T) -> True
   bool(F) -> True
   bool(And(z0, z1)) -> False
   bool(Or(z0, z1)) -> False
   isConsTerm(T, T) -> True
   isConsTerm(T, F) -> False
   isConsTerm(T, And(z0, z1)) -> False
   isConsTerm(T, Or(z0, z1)) -> False
   isConsTerm(F, T) -> False
   isConsTerm(F, F) -> True
   isConsTerm(F, And(z0, z1)) -> False
   isConsTerm(F, Or(z0, z1)) -> False
   isConsTerm(And(z0, z1), T) -> False
   isConsTerm(And(z0, z1), F) -> False
   isConsTerm(And(z0, z1), And(z2, z3)) -> True
   isConsTerm(And(z0, z1), Or(z2, z3)) -> False
   isConsTerm(Or(z0, z1), T) -> False
   isConsTerm(Or(z0, z1), F) -> False
   isConsTerm(Or(z0, z1), And(z2, z3)) -> False
   isConsTerm(Or(z0, z1), Or(z2, z3)) -> True
   isOp(T) -> False
   isOp(F) -> False
   isOp(And(z0, z1)) -> True
   isOp(Or(z0, z1)) -> True
   isAnd(T) -> False
   isAnd(F) -> False
   isAnd(And(z0, z1)) -> True
   isAnd(Or(z0, z1)) -> False
   getSecond(And(z0, z1)) -> z0
   getSecond(Or(z0, z1)) -> z0
   getFirst(And(z0, z1)) -> z0
   getFirst(Or(z0, z1)) -> z0
   disjconj(z0) -> disj(z0)
Tuples:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   DISJ(T) -> c4
   DISJ(F) -> c5
   DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
   DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
   DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
   CONJ(Or(z0, z1)) -> c9
   CONJ(T) -> c10
   CONJ(F) -> c11
   CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
   CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
   BOOL(T) -> c14
   BOOL(F) -> c15
   BOOL(And(z0, z1)) -> c16
   BOOL(Or(z0, z1)) -> c17
   ISCONSTERM(T, T) -> c18
   ISCONSTERM(T, F) -> c19
   ISCONSTERM(T, And(z0, z1)) -> c20
   ISCONSTERM(T, Or(z0, z1)) -> c21
   ISCONSTERM(F, T) -> c22
   ISCONSTERM(F, F) -> c23
   ISCONSTERM(F, And(z0, z1)) -> c24
   ISCONSTERM(F, Or(z0, z1)) -> c25
   ISCONSTERM(And(z0, z1), T) -> c26
   ISCONSTERM(And(z0, z1), F) -> c27
   ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
   ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
   ISCONSTERM(Or(z0, z1), T) -> c30
   ISCONSTERM(Or(z0, z1), F) -> c31
   ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
   ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
   ISOP(T) -> c34
   ISOP(F) -> c35
   ISOP(And(z0, z1)) -> c36
   ISOP(Or(z0, z1)) -> c37
   ISAND(T) -> c38
   ISAND(F) -> c39
   ISAND(And(z0, z1)) -> c40
   ISAND(Or(z0, z1)) -> c41
   GETSECOND(And(z0, z1)) -> c42
   GETSECOND(Or(z0, z1)) -> c43
   GETFIRST(And(z0, z1)) -> c44
   GETFIRST(Or(z0, z1)) -> c45
   DISJCONJ(z0) -> c46(DISJ(z0))
S tuples:
   DISJ(T) -> c4
   DISJ(F) -> c5
   DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
   DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
   DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
   CONJ(Or(z0, z1)) -> c9
   CONJ(T) -> c10
   CONJ(F) -> c11
   CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
   CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
   BOOL(T) -> c14
   BOOL(F) -> c15
   BOOL(And(z0, z1)) -> c16
   BOOL(Or(z0, z1)) -> c17
   ISCONSTERM(T, T) -> c18
   ISCONSTERM(T, F) -> c19
   ISCONSTERM(T, And(z0, z1)) -> c20
   ISCONSTERM(T, Or(z0, z1)) -> c21
   ISCONSTERM(F, T) -> c22
   ISCONSTERM(F, F) -> c23
   ISCONSTERM(F, And(z0, z1)) -> c24
   ISCONSTERM(F, Or(z0, z1)) -> c25
   ISCONSTERM(And(z0, z1), T) -> c26
   ISCONSTERM(And(z0, z1), F) -> c27
   ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
   ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
   ISCONSTERM(Or(z0, z1), T) -> c30
   ISCONSTERM(Or(z0, z1), F) -> c31
   ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
   ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
   ISOP(T) -> c34
   ISOP(F) -> c35
   ISOP(And(z0, z1)) -> c36
   ISOP(Or(z0, z1)) -> c37
   ISAND(T) -> c38
   ISAND(F) -> c39
   ISAND(And(z0, z1)) -> c40
   ISAND(Or(z0, z1)) -> c41
   GETSECOND(And(z0, z1)) -> c42
   GETSECOND(Or(z0, z1)) -> c43
   GETFIRST(And(z0, z1)) -> c44
   GETFIRST(Or(z0, z1)) -> c45
   DISJCONJ(z0) -> c46(DISJ(z0))
K tuples:none
Defined Rule Symbols:   disj_1, conj_1, bool_1, isConsTerm_2, isOp_1, isAnd_1, getSecond_1, getFirst_1, disjconj_1, and_2

Defined Pair Symbols:   AND_2, DISJ_1, CONJ_1, BOOL_1, ISCONSTERM_2, ISOP_1, ISAND_1, GETSECOND_1, GETFIRST_1, DISJCONJ_1

Compound Symbols:   c, c1, c2, c3, c4, c5, c6_1, c7_2, c8_2, c9, c10, c11, c12_2, c13_2, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46_1


----------------------------------------

(5) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   DISJ(T) -> c4
   DISJ(F) -> c5
   DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
   DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
   DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
   CONJ(Or(z0, z1)) -> c9
   CONJ(T) -> c10
   CONJ(F) -> c11
   CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
   CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
   BOOL(T) -> c14
   BOOL(F) -> c15
   BOOL(And(z0, z1)) -> c16
   BOOL(Or(z0, z1)) -> c17
   ISCONSTERM(T, T) -> c18
   ISCONSTERM(T, F) -> c19
   ISCONSTERM(T, And(z0, z1)) -> c20
   ISCONSTERM(T, Or(z0, z1)) -> c21
   ISCONSTERM(F, T) -> c22
   ISCONSTERM(F, F) -> c23
   ISCONSTERM(F, And(z0, z1)) -> c24
   ISCONSTERM(F, Or(z0, z1)) -> c25
   ISCONSTERM(And(z0, z1), T) -> c26
   ISCONSTERM(And(z0, z1), F) -> c27
   ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
   ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
   ISCONSTERM(Or(z0, z1), T) -> c30
   ISCONSTERM(Or(z0, z1), F) -> c31
   ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
   ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
   ISOP(T) -> c34
   ISOP(F) -> c35
   ISOP(And(z0, z1)) -> c36
   ISOP(Or(z0, z1)) -> c37
   ISAND(T) -> c38
   ISAND(F) -> c39
   ISAND(And(z0, z1)) -> c40
   ISAND(Or(z0, z1)) -> c41
   GETSECOND(And(z0, z1)) -> c42
   GETSECOND(Or(z0, z1)) -> c43
   GETFIRST(And(z0, z1)) -> c44
   GETFIRST(Or(z0, z1)) -> c45
   DISJCONJ(z0) -> c46(DISJ(z0))

The (relative) TRS S consists of the following rules:

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   disj(T) -> True
   disj(F) -> True
   disj(And(z0, z1)) -> conj(And(z0, z1))
   disj(Or(z0, z1)) -> and(conj(z0), disj(z0))
   conj(Or(z0, z1)) -> False
   conj(T) -> True
   conj(F) -> True
   conj(And(z0, z1)) -> and(disj(z0), conj(z0))
   bool(T) -> True
   bool(F) -> True
   bool(And(z0, z1)) -> False
   bool(Or(z0, z1)) -> False
   isConsTerm(T, T) -> True
   isConsTerm(T, F) -> False
   isConsTerm(T, And(z0, z1)) -> False
   isConsTerm(T, Or(z0, z1)) -> False
   isConsTerm(F, T) -> False
   isConsTerm(F, F) -> True
   isConsTerm(F, And(z0, z1)) -> False
   isConsTerm(F, Or(z0, z1)) -> False
   isConsTerm(And(z0, z1), T) -> False
   isConsTerm(And(z0, z1), F) -> False
   isConsTerm(And(z0, z1), And(z2, z3)) -> True
   isConsTerm(And(z0, z1), Or(z2, z3)) -> False
   isConsTerm(Or(z0, z1), T) -> False
   isConsTerm(Or(z0, z1), F) -> False
   isConsTerm(Or(z0, z1), And(z2, z3)) -> False
   isConsTerm(Or(z0, z1), Or(z2, z3)) -> True
   isOp(T) -> False
   isOp(F) -> False
   isOp(And(z0, z1)) -> True
   isOp(Or(z0, z1)) -> True
   isAnd(T) -> False
   isAnd(F) -> False
   isAnd(And(z0, z1)) -> True
   isAnd(Or(z0, z1)) -> False
   getSecond(And(z0, z1)) -> z0
   getSecond(Or(z0, z1)) -> z0
   getFirst(And(z0, z1)) -> z0
   getFirst(Or(z0, z1)) -> z0
   disjconj(z0) -> disj(z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(7) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(8)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF).


The TRS R consists of the following rules:

   DISJ(T) -> c4
   DISJ(F) -> c5
   DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
   DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
   DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
   CONJ(Or(z0, z1)) -> c9
   CONJ(T) -> c10
   CONJ(F) -> c11
   CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
   CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
   BOOL(T) -> c14
   BOOL(F) -> c15
   BOOL(And(z0, z1)) -> c16
   BOOL(Or(z0, z1)) -> c17
   ISCONSTERM(T, T) -> c18
   ISCONSTERM(T, F) -> c19
   ISCONSTERM(T, And(z0, z1)) -> c20
   ISCONSTERM(T, Or(z0, z1)) -> c21
   ISCONSTERM(F, T) -> c22
   ISCONSTERM(F, F) -> c23
   ISCONSTERM(F, And(z0, z1)) -> c24
   ISCONSTERM(F, Or(z0, z1)) -> c25
   ISCONSTERM(And(z0, z1), T) -> c26
   ISCONSTERM(And(z0, z1), F) -> c27
   ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
   ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
   ISCONSTERM(Or(z0, z1), T) -> c30
   ISCONSTERM(Or(z0, z1), F) -> c31
   ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
   ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
   ISOP(T) -> c34
   ISOP(F) -> c35
   ISOP(And(z0, z1)) -> c36
   ISOP(Or(z0, z1)) -> c37
   ISAND(T) -> c38
   ISAND(F) -> c39
   ISAND(And(z0, z1)) -> c40
   ISAND(Or(z0, z1)) -> c41
   GETSECOND(And(z0, z1)) -> c42
   GETSECOND(Or(z0, z1)) -> c43
   GETFIRST(And(z0, z1)) -> c44
   GETFIRST(Or(z0, z1)) -> c45
   DISJCONJ(z0) -> c46(DISJ(z0))

The (relative) TRS S consists of the following rules:

   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   disj(T) -> True
   disj(F) -> True
   disj(And(z0, z1)) -> conj(And(z0, z1))
   disj(Or(z0, z1)) -> and(conj(z0), disj(z0))
   conj(Or(z0, z1)) -> False
   conj(T) -> True
   conj(F) -> True
   conj(And(z0, z1)) -> and(disj(z0), conj(z0))
   bool(T) -> True
   bool(F) -> True
   bool(And(z0, z1)) -> False
   bool(Or(z0, z1)) -> False
   isConsTerm(T, T) -> True
   isConsTerm(T, F) -> False
   isConsTerm(T, And(z0, z1)) -> False
   isConsTerm(T, Or(z0, z1)) -> False
   isConsTerm(F, T) -> False
   isConsTerm(F, F) -> True
   isConsTerm(F, And(z0, z1)) -> False
   isConsTerm(F, Or(z0, z1)) -> False
   isConsTerm(And(z0, z1), T) -> False
   isConsTerm(And(z0, z1), F) -> False
   isConsTerm(And(z0, z1), And(z2, z3)) -> True
   isConsTerm(And(z0, z1), Or(z2, z3)) -> False
   isConsTerm(Or(z0, z1), T) -> False
   isConsTerm(Or(z0, z1), F) -> False
   isConsTerm(Or(z0, z1), And(z2, z3)) -> False
   isConsTerm(Or(z0, z1), Or(z2, z3)) -> True
   isOp(T) -> False
   isOp(F) -> False
   isOp(And(z0, z1)) -> True
   isOp(Or(z0, z1)) -> True
   isAnd(T) -> False
   isAnd(F) -> False
   isAnd(And(z0, z1)) -> True
   isAnd(Or(z0, z1)) -> False
   getSecond(And(z0, z1)) -> z0
   getSecond(Or(z0, z1)) -> z0
   getFirst(And(z0, z1)) -> z0
   getFirst(Or(z0, z1)) -> z0
   disjconj(z0) -> disj(z0)

Rewrite Strategy: INNERMOST
----------------------------------------

(9) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
DISJ(T) -> c4
DISJ(F) -> c5
DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
CONJ(Or(z0, z1)) -> c9
CONJ(T) -> c10
CONJ(F) -> c11
CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
BOOL(T) -> c14
BOOL(F) -> c15
BOOL(And(z0, z1)) -> c16
BOOL(Or(z0, z1)) -> c17
ISCONSTERM(T, T) -> c18
ISCONSTERM(T, F) -> c19
ISCONSTERM(T, And(z0, z1)) -> c20
ISCONSTERM(T, Or(z0, z1)) -> c21
ISCONSTERM(F, T) -> c22
ISCONSTERM(F, F) -> c23
ISCONSTERM(F, And(z0, z1)) -> c24
ISCONSTERM(F, Or(z0, z1)) -> c25
ISCONSTERM(And(z0, z1), T) -> c26
ISCONSTERM(And(z0, z1), F) -> c27
ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
ISCONSTERM(Or(z0, z1), T) -> c30
ISCONSTERM(Or(z0, z1), F) -> c31
ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
ISOP(T) -> c34
ISOP(F) -> c35
ISOP(And(z0, z1)) -> c36
ISOP(Or(z0, z1)) -> c37
ISAND(T) -> c38
ISAND(F) -> c39
ISAND(And(z0, z1)) -> c40
ISAND(Or(z0, z1)) -> c41
GETSECOND(And(z0, z1)) -> c42
GETSECOND(Or(z0, z1)) -> c43
GETFIRST(And(z0, z1)) -> c44
GETFIRST(Or(z0, z1)) -> c45
DISJCONJ(z0) -> c46(DISJ(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
disj(T) -> True
disj(F) -> True
disj(And(z0, z1)) -> conj(And(z0, z1))
disj(Or(z0, z1)) -> and(conj(z0), disj(z0))
conj(Or(z0, z1)) -> False
conj(T) -> True
conj(F) -> True
conj(And(z0, z1)) -> and(disj(z0), conj(z0))
bool(T) -> True
bool(F) -> True
bool(And(z0, z1)) -> False
bool(Or(z0, z1)) -> False
isConsTerm(T, T) -> True
isConsTerm(T, F) -> False
isConsTerm(T, And(z0, z1)) -> False
isConsTerm(T, Or(z0, z1)) -> False
isConsTerm(F, T) -> False
isConsTerm(F, F) -> True
isConsTerm(F, And(z0, z1)) -> False
isConsTerm(F, Or(z0, z1)) -> False
isConsTerm(And(z0, z1), T) -> False
isConsTerm(And(z0, z1), F) -> False
isConsTerm(And(z0, z1), And(z2, z3)) -> True
isConsTerm(And(z0, z1), Or(z2, z3)) -> False
isConsTerm(Or(z0, z1), T) -> False
isConsTerm(Or(z0, z1), F) -> False
isConsTerm(Or(z0, z1), And(z2, z3)) -> False
isConsTerm(Or(z0, z1), Or(z2, z3)) -> True
isOp(T) -> False
isOp(F) -> False
isOp(And(z0, z1)) -> True
isOp(Or(z0, z1)) -> True
isAnd(T) -> False
isAnd(F) -> False
isAnd(And(z0, z1)) -> True
isAnd(Or(z0, z1)) -> False
getSecond(And(z0, z1)) -> z0
getSecond(Or(z0, z1)) -> z0
getFirst(And(z0, z1)) -> z0
getFirst(Or(z0, z1)) -> z0
disjconj(z0) -> disj(z0)

Types:
DISJ :: T:F:And:Or -> c4:c5:c6:c7:c8
T :: T:F:And:Or
c4 :: c4:c5:c6:c7:c8
F :: T:F:And:Or
c5 :: c4:c5:c6:c7:c8
And :: T:F:And:Or -> a -> T:F:And:Or
c6 :: c9:c10:c11:c12:c13 -> c4:c5:c6:c7:c8
CONJ :: T:F:And:Or -> c9:c10:c11:c12:c13
Or :: T:F:And:Or -> b -> T:F:And:Or
c7 :: c:c1:c2:c3 -> c9:c10:c11:c12:c13 -> c4:c5:c6:c7:c8
AND :: False:True -> False:True -> c:c1:c2:c3
conj :: T:F:And:Or -> False:True
disj :: T:F:And:Or -> False:True
c8 :: c:c1:c2:c3 -> c4:c5:c6:c7:c8 -> c4:c5:c6:c7:c8
c9 :: c9:c10:c11:c12:c13
c10 :: c9:c10:c11:c12:c13
c11 :: c9:c10:c11:c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6:c7:c8 -> c9:c10:c11:c12:c13
c13 :: c:c1:c2:c3 -> c9:c10:c11:c12:c13 -> c9:c10:c11:c12:c13
BOOL :: T:F:And:Or -> c14:c15:c16:c17
c14 :: c14:c15:c16:c17
c15 :: c14:c15:c16:c17
c16 :: c14:c15:c16:c17
c17 :: c14:c15:c16:c17
ISCONSTERM :: T:F:And:Or -> T:F:And:Or -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c18 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c19 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c20 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c21 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c22 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c23 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c24 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c25 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c26 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c33 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
ISOP :: T:F:And:Or -> c34:c35:c36:c37
c34 :: c34:c35:c36:c37
c35 :: c34:c35:c36:c37
c36 :: c34:c35:c36:c37
c37 :: c34:c35:c36:c37
ISAND :: T:F:And:Or -> c38:c39:c40:c41
c38 :: c38:c39:c40:c41
c39 :: c38:c39:c40:c41
c40 :: c38:c39:c40:c41
c41 :: c38:c39:c40:c41
GETSECOND :: T:F:And:Or -> c42:c43
c42 :: c42:c43
c43 :: c42:c43
GETFIRST :: T:F:And:Or -> c44:c45
c44 :: c44:c45
c45 :: c44:c45
DISJCONJ :: T:F:And:Or -> c46
c46 :: c4:c5:c6:c7:c8 -> c46
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
bool :: T:F:And:Or -> False:True
isConsTerm :: T:F:And:Or -> T:F:And:Or -> False:True
isOp :: T:F:And:Or -> False:True
isAnd :: T:F:And:Or -> False:True
getSecond :: T:F:And:Or -> T:F:And:Or
getFirst :: T:F:And:Or -> T:F:And:Or
disjconj :: T:F:And:Or -> False:True
hole_c4:c5:c6:c7:c81_47 :: c4:c5:c6:c7:c8
hole_T:F:And:Or2_47 :: T:F:And:Or
hole_a3_47 :: a
hole_c9:c10:c11:c12:c134_47 :: c9:c10:c11:c12:c13
hole_b5_47 :: b
hole_c:c1:c2:c36_47 :: c:c1:c2:c3
hole_False:True7_47 :: False:True
hole_c14:c15:c16:c178_47 :: c14:c15:c16:c17
hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c339_47 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
hole_c34:c35:c36:c3710_47 :: c34:c35:c36:c37
hole_c38:c39:c40:c4111_47 :: c38:c39:c40:c41
hole_c42:c4312_47 :: c42:c43
hole_c44:c4513_47 :: c44:c45
hole_c4614_47 :: c46
gen_c4:c5:c6:c7:c815_47 :: Nat -> c4:c5:c6:c7:c8
gen_T:F:And:Or16_47 :: Nat -> T:F:And:Or
gen_c9:c10:c11:c12:c1317_47 :: Nat -> c9:c10:c11:c12:c13

----------------------------------------

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
DISJ, CONJ, conj, disj

They will be analysed ascendingly in the following order:
DISJ = CONJ
conj < DISJ
disj < DISJ
conj < CONJ
disj < CONJ
conj = disj

----------------------------------------

(12)
Obligation:
Innermost TRS:
Rules:
DISJ(T) -> c4
DISJ(F) -> c5
DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
CONJ(Or(z0, z1)) -> c9
CONJ(T) -> c10
CONJ(F) -> c11
CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
BOOL(T) -> c14
BOOL(F) -> c15
BOOL(And(z0, z1)) -> c16
BOOL(Or(z0, z1)) -> c17
ISCONSTERM(T, T) -> c18
ISCONSTERM(T, F) -> c19
ISCONSTERM(T, And(z0, z1)) -> c20
ISCONSTERM(T, Or(z0, z1)) -> c21
ISCONSTERM(F, T) -> c22
ISCONSTERM(F, F) -> c23
ISCONSTERM(F, And(z0, z1)) -> c24
ISCONSTERM(F, Or(z0, z1)) -> c25
ISCONSTERM(And(z0, z1), T) -> c26
ISCONSTERM(And(z0, z1), F) -> c27
ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
ISCONSTERM(Or(z0, z1), T) -> c30
ISCONSTERM(Or(z0, z1), F) -> c31
ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
ISOP(T) -> c34
ISOP(F) -> c35
ISOP(And(z0, z1)) -> c36
ISOP(Or(z0, z1)) -> c37
ISAND(T) -> c38
ISAND(F) -> c39
ISAND(And(z0, z1)) -> c40
ISAND(Or(z0, z1)) -> c41
GETSECOND(And(z0, z1)) -> c42
GETSECOND(Or(z0, z1)) -> c43
GETFIRST(And(z0, z1)) -> c44
GETFIRST(Or(z0, z1)) -> c45
DISJCONJ(z0) -> c46(DISJ(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
disj(T) -> True
disj(F) -> True
disj(And(z0, z1)) -> conj(And(z0, z1))
disj(Or(z0, z1)) -> and(conj(z0), disj(z0))
conj(Or(z0, z1)) -> False
conj(T) -> True
conj(F) -> True
conj(And(z0, z1)) -> and(disj(z0), conj(z0))
bool(T) -> True
bool(F) -> True
bool(And(z0, z1)) -> False
bool(Or(z0, z1)) -> False
isConsTerm(T, T) -> True
isConsTerm(T, F) -> False
isConsTerm(T, And(z0, z1)) -> False
isConsTerm(T, Or(z0, z1)) -> False
isConsTerm(F, T) -> False
isConsTerm(F, F) -> True
isConsTerm(F, And(z0, z1)) -> False
isConsTerm(F, Or(z0, z1)) -> False
isConsTerm(And(z0, z1), T) -> False
isConsTerm(And(z0, z1), F) -> False
isConsTerm(And(z0, z1), And(z2, z3)) -> True
isConsTerm(And(z0, z1), Or(z2, z3)) -> False
isConsTerm(Or(z0, z1), T) -> False
isConsTerm(Or(z0, z1), F) -> False
isConsTerm(Or(z0, z1), And(z2, z3)) -> False
isConsTerm(Or(z0, z1), Or(z2, z3)) -> True
isOp(T) -> False
isOp(F) -> False
isOp(And(z0, z1)) -> True
isOp(Or(z0, z1)) -> True
isAnd(T) -> False
isAnd(F) -> False
isAnd(And(z0, z1)) -> True
isAnd(Or(z0, z1)) -> False
getSecond(And(z0, z1)) -> z0
getSecond(Or(z0, z1)) -> z0
getFirst(And(z0, z1)) -> z0
getFirst(Or(z0, z1)) -> z0
disjconj(z0) -> disj(z0)

Types:
DISJ :: T:F:And:Or -> c4:c5:c6:c7:c8
T :: T:F:And:Or
c4 :: c4:c5:c6:c7:c8
F :: T:F:And:Or
c5 :: c4:c5:c6:c7:c8
And :: T:F:And:Or -> a -> T:F:And:Or
c6 :: c9:c10:c11:c12:c13 -> c4:c5:c6:c7:c8
CONJ :: T:F:And:Or -> c9:c10:c11:c12:c13
Or :: T:F:And:Or -> b -> T:F:And:Or
c7 :: c:c1:c2:c3 -> c9:c10:c11:c12:c13 -> c4:c5:c6:c7:c8
AND :: False:True -> False:True -> c:c1:c2:c3
conj :: T:F:And:Or -> False:True
disj :: T:F:And:Or -> False:True
c8 :: c:c1:c2:c3 -> c4:c5:c6:c7:c8 -> c4:c5:c6:c7:c8
c9 :: c9:c10:c11:c12:c13
c10 :: c9:c10:c11:c12:c13
c11 :: c9:c10:c11:c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6:c7:c8 -> c9:c10:c11:c12:c13
c13 :: c:c1:c2:c3 -> c9:c10:c11:c12:c13 -> c9:c10:c11:c12:c13
BOOL :: T:F:And:Or -> c14:c15:c16:c17
c14 :: c14:c15:c16:c17
c15 :: c14:c15:c16:c17
c16 :: c14:c15:c16:c17
c17 :: c14:c15:c16:c17
ISCONSTERM :: T:F:And:Or -> T:F:And:Or -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c18 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c19 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c20 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c21 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c22 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c23 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c24 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c25 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c26 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c33 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
ISOP :: T:F:And:Or -> c34:c35:c36:c37
c34 :: c34:c35:c36:c37
c35 :: c34:c35:c36:c37
c36 :: c34:c35:c36:c37
c37 :: c34:c35:c36:c37
ISAND :: T:F:And:Or -> c38:c39:c40:c41
c38 :: c38:c39:c40:c41
c39 :: c38:c39:c40:c41
c40 :: c38:c39:c40:c41
c41 :: c38:c39:c40:c41
GETSECOND :: T:F:And:Or -> c42:c43
c42 :: c42:c43
c43 :: c42:c43
GETFIRST :: T:F:And:Or -> c44:c45
c44 :: c44:c45
c45 :: c44:c45
DISJCONJ :: T:F:And:Or -> c46
c46 :: c4:c5:c6:c7:c8 -> c46
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
bool :: T:F:And:Or -> False:True
isConsTerm :: T:F:And:Or -> T:F:And:Or -> False:True
isOp :: T:F:And:Or -> False:True
isAnd :: T:F:And:Or -> False:True
getSecond :: T:F:And:Or -> T:F:And:Or
getFirst :: T:F:And:Or -> T:F:And:Or
disjconj :: T:F:And:Or -> False:True
hole_c4:c5:c6:c7:c81_47 :: c4:c5:c6:c7:c8
hole_T:F:And:Or2_47 :: T:F:And:Or
hole_a3_47 :: a
hole_c9:c10:c11:c12:c134_47 :: c9:c10:c11:c12:c13
hole_b5_47 :: b
hole_c:c1:c2:c36_47 :: c:c1:c2:c3
hole_False:True7_47 :: False:True
hole_c14:c15:c16:c178_47 :: c14:c15:c16:c17
hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c339_47 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
hole_c34:c35:c36:c3710_47 :: c34:c35:c36:c37
hole_c38:c39:c40:c4111_47 :: c38:c39:c40:c41
hole_c42:c4312_47 :: c42:c43
hole_c44:c4513_47 :: c44:c45
hole_c4614_47 :: c46
gen_c4:c5:c6:c7:c815_47 :: Nat -> c4:c5:c6:c7:c8
gen_T:F:And:Or16_47 :: Nat -> T:F:And:Or
gen_c9:c10:c11:c12:c1317_47 :: Nat -> c9:c10:c11:c12:c13


Generator Equations:
gen_c4:c5:c6:c7:c815_47(0) <=> c4
gen_c4:c5:c6:c7:c815_47(+(x, 1)) <=> c8(c, gen_c4:c5:c6:c7:c815_47(x))
gen_T:F:And:Or16_47(0) <=> T
gen_T:F:And:Or16_47(+(x, 1)) <=> And(gen_T:F:And:Or16_47(x), hole_a3_47)
gen_c9:c10:c11:c12:c1317_47(0) <=> c9
gen_c9:c10:c11:c12:c1317_47(+(x, 1)) <=> c13(c, gen_c9:c10:c11:c12:c1317_47(x))


The following defined symbols remain to be analysed:
disj, DISJ, CONJ, conj

They will be analysed ascendingly in the following order:
DISJ = CONJ
conj < DISJ
disj < DISJ
conj < CONJ
disj < CONJ
conj = disj

----------------------------------------

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
disj(gen_T:F:And:Or16_47(n19_47)) -> *18_47, rt in Omega(0)

Induction Base:
disj(gen_T:F:And:Or16_47(0))

Induction Step:
disj(gen_T:F:And:Or16_47(+(n19_47, 1))) ->_R^Omega(0)
conj(And(gen_T:F:And:Or16_47(n19_47), hole_a3_47)) ->_R^Omega(0)
and(disj(gen_T:F:And:Or16_47(n19_47)), conj(gen_T:F:And:Or16_47(n19_47))) ->_IH
and(*18_47, conj(gen_T:F:And:Or16_47(n19_47)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
DISJ(T) -> c4
DISJ(F) -> c5
DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1)))
DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
CONJ(Or(z0, z1)) -> c9
CONJ(T) -> c10
CONJ(F) -> c11
CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
BOOL(T) -> c14
BOOL(F) -> c15
BOOL(And(z0, z1)) -> c16
BOOL(Or(z0, z1)) -> c17
ISCONSTERM(T, T) -> c18
ISCONSTERM(T, F) -> c19
ISCONSTERM(T, And(z0, z1)) -> c20
ISCONSTERM(T, Or(z0, z1)) -> c21
ISCONSTERM(F, T) -> c22
ISCONSTERM(F, F) -> c23
ISCONSTERM(F, And(z0, z1)) -> c24
ISCONSTERM(F, Or(z0, z1)) -> c25
ISCONSTERM(And(z0, z1), T) -> c26
ISCONSTERM(And(z0, z1), F) -> c27
ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28
ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29
ISCONSTERM(Or(z0, z1), T) -> c30
ISCONSTERM(Or(z0, z1), F) -> c31
ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32
ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33
ISOP(T) -> c34
ISOP(F) -> c35
ISOP(And(z0, z1)) -> c36
ISOP(Or(z0, z1)) -> c37
ISAND(T) -> c38
ISAND(F) -> c39
ISAND(And(z0, z1)) -> c40
ISAND(Or(z0, z1)) -> c41
GETSECOND(And(z0, z1)) -> c42
GETSECOND(Or(z0, z1)) -> c43
GETFIRST(And(z0, z1)) -> c44
GETFIRST(Or(z0, z1)) -> c45
DISJCONJ(z0) -> c46(DISJ(z0))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
disj(T) -> True
disj(F) -> True
disj(And(z0, z1)) -> conj(And(z0, z1))
disj(Or(z0, z1)) -> and(conj(z0), disj(z0))
conj(Or(z0, z1)) -> False
conj(T) -> True
conj(F) -> True
conj(And(z0, z1)) -> and(disj(z0), conj(z0))
bool(T) -> True
bool(F) -> True
bool(And(z0, z1)) -> False
bool(Or(z0, z1)) -> False
isConsTerm(T, T) -> True
isConsTerm(T, F) -> False
isConsTerm(T, And(z0, z1)) -> False
isConsTerm(T, Or(z0, z1)) -> False
isConsTerm(F, T) -> False
isConsTerm(F, F) -> True
isConsTerm(F, And(z0, z1)) -> False
isConsTerm(F, Or(z0, z1)) -> False
isConsTerm(And(z0, z1), T) -> False
isConsTerm(And(z0, z1), F) -> False
isConsTerm(And(z0, z1), And(z2, z3)) -> True
isConsTerm(And(z0, z1), Or(z2, z3)) -> False
isConsTerm(Or(z0, z1), T) -> False
isConsTerm(Or(z0, z1), F) -> False
isConsTerm(Or(z0, z1), And(z2, z3)) -> False
isConsTerm(Or(z0, z1), Or(z2, z3)) -> True
isOp(T) -> False
isOp(F) -> False
isOp(And(z0, z1)) -> True
isOp(Or(z0, z1)) -> True
isAnd(T) -> False
isAnd(F) -> False
isAnd(And(z0, z1)) -> True
isAnd(Or(z0, z1)) -> False
getSecond(And(z0, z1)) -> z0
getSecond(Or(z0, z1)) -> z0
getFirst(And(z0, z1)) -> z0
getFirst(Or(z0, z1)) -> z0
disjconj(z0) -> disj(z0)

Types:
DISJ :: T:F:And:Or -> c4:c5:c6:c7:c8
T :: T:F:And:Or
c4 :: c4:c5:c6:c7:c8
F :: T:F:And:Or
c5 :: c4:c5:c6:c7:c8
And :: T:F:And:Or -> a -> T:F:And:Or
c6 :: c9:c10:c11:c12:c13 -> c4:c5:c6:c7:c8
CONJ :: T:F:And:Or -> c9:c10:c11:c12:c13
Or :: T:F:And:Or -> b -> T:F:And:Or
c7 :: c:c1:c2:c3 -> c9:c10:c11:c12:c13 -> c4:c5:c6:c7:c8
AND :: False:True -> False:True -> c:c1:c2:c3
conj :: T:F:And:Or -> False:True
disj :: T:F:And:Or -> False:True
c8 :: c:c1:c2:c3 -> c4:c5:c6:c7:c8 -> c4:c5:c6:c7:c8
c9 :: c9:c10:c11:c12:c13
c10 :: c9:c10:c11:c12:c13
c11 :: c9:c10:c11:c12:c13
c12 :: c:c1:c2:c3 -> c4:c5:c6:c7:c8 -> c9:c10:c11:c12:c13
c13 :: c:c1:c2:c3 -> c9:c10:c11:c12:c13 -> c9:c10:c11:c12:c13
BOOL :: T:F:And:Or -> c14:c15:c16:c17
c14 :: c14:c15:c16:c17
c15 :: c14:c15:c16:c17
c16 :: c14:c15:c16:c17
c17 :: c14:c15:c16:c17
ISCONSTERM :: T:F:And:Or -> T:F:And:Or -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c18 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c19 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c20 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c21 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c22 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c23 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c24 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c25 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c26 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
c33 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
ISOP :: T:F:And:Or -> c34:c35:c36:c37
c34 :: c34:c35:c36:c37
c35 :: c34:c35:c36:c37
c36 :: c34:c35:c36:c37
c37 :: c34:c35:c36:c37
ISAND :: T:F:And:Or -> c38:c39:c40:c41
c38 :: c38:c39:c40:c41
c39 :: c38:c39:c40:c41
c40 :: c38:c39:c40:c41
c41 :: c38:c39:c40:c41
GETSECOND :: T:F:And:Or -> c42:c43
c42 :: c42:c43
c43 :: c42:c43
GETFIRST :: T:F:And:Or -> c44:c45
c44 :: c44:c45
c45 :: c44:c45
DISJCONJ :: T:F:And:Or -> c46
c46 :: c4:c5:c6:c7:c8 -> c46
False :: False:True
c :: c:c1:c2:c3
True :: False:True
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
and :: False:True -> False:True -> False:True
bool :: T:F:And:Or -> False:True
isConsTerm :: T:F:And:Or -> T:F:And:Or -> False:True
isOp :: T:F:And:Or -> False:True
isAnd :: T:F:And:Or -> False:True
getSecond :: T:F:And:Or -> T:F:And:Or
getFirst :: T:F:And:Or -> T:F:And:Or
disjconj :: T:F:And:Or -> False:True
hole_c4:c5:c6:c7:c81_47 :: c4:c5:c6:c7:c8
hole_T:F:And:Or2_47 :: T:F:And:Or
hole_a3_47 :: a
hole_c9:c10:c11:c12:c134_47 :: c9:c10:c11:c12:c13
hole_b5_47 :: b
hole_c:c1:c2:c36_47 :: c:c1:c2:c3
hole_False:True7_47 :: False:True
hole_c14:c15:c16:c178_47 :: c14:c15:c16:c17
hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c339_47 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
hole_c34:c35:c36:c3710_47 :: c34:c35:c36:c37
hole_c38:c39:c40:c4111_47 :: c38:c39:c40:c41
hole_c42:c4312_47 :: c42:c43
hole_c44:c4513_47 :: c44:c45
hole_c4614_47 :: c46
gen_c4:c5:c6:c7:c815_47 :: Nat -> c4:c5:c6:c7:c8
gen_T:F:And:Or16_47 :: Nat -> T:F:And:Or
gen_c9:c10:c11:c12:c1317_47 :: Nat -> c9:c10:c11:c12:c13


Lemmas:
disj(gen_T:F:And:Or16_47(n19_47)) -> *18_47, rt in Omega(0)


Generator Equations:
gen_c4:c5:c6:c7:c815_47(0) <=> c4
gen_c4:c5:c6:c7:c815_47(+(x, 1)) <=> c8(c, gen_c4:c5:c6:c7:c815_47(x))
gen_T:F:And:Or16_47(0) <=> T
gen_T:F:And:Or16_47(+(x, 1)) <=> And(gen_T:F:And:Or16_47(x), hole_a3_47)
gen_c9:c10:c11:c12:c1317_47(0) <=> c9
gen_c9:c10:c11:c12:c1317_47(+(x, 1)) <=> c13(c, gen_c9:c10:c11:c12:c1317_47(x))


The following defined symbols remain to be analysed:
conj, DISJ, CONJ

They will be analysed ascendingly in the following order:
DISJ = CONJ
conj < DISJ
disj < DISJ
conj < CONJ
disj < CONJ
conj = disj

----------------------------------------

(15) RewriteLemmaProof (FINISHED)
Proved the following rewrite lemma:
conj(gen_T:F:And:Or16_47(+(1, n15357_47))) -> *18_47, rt in Omega(EXP)

Induction Base:
conj(gen_T:F:And:Or16_47(+(1, 0)))

Induction Step:
conj(gen_T:F:And:Or16_47(+(1, +(n15357_47, 1)))) ->_R^Omega(0)
and(disj(gen_T:F:And:Or16_47(+(1, n15357_47))), conj(gen_T:F:And:Or16_47(+(1, n15357_47)))) ->_R^Omega(0)
and(conj(And(gen_T:F:And:Or16_47(n15357_47), hole_a3_47)), conj(gen_T:F:And:Or16_47(+(1, n15357_47)))) ->_IH
and(*18_47, conj(gen_T:F:And:Or16_47(+(1, n15357_47)))) ->_IH
and(*18_47, *18_47)

We have rt in EXP and sz in O(n). Thus, we have irc_R in EXP
----------------------------------------

(16)
BOUNDS(EXP, INF)