WORST_CASE(NON_POLY,?)
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(EXP, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 439 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), 28 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 911 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [FINISHED, 486 ms]
(14) BOUNDS(EXP, INF)


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

(0)
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
----------------------------------------

(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(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
----------------------------------------

(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(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
----------------------------------------

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
And/1
Or/1

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

(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)) -> c6(CONJ(And(z0)))
   DISJ(Or(z0)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
   DISJ(Or(z0)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
   CONJ(Or(z0)) -> c9
   CONJ(T) -> c10
   CONJ(F) -> c11
   CONJ(And(z0)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
   CONJ(And(z0)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
   BOOL(T) -> c14
   BOOL(F) -> c15
   BOOL(And(z0)) -> c16
   BOOL(Or(z0)) -> c17
   ISCONSTERM(T, T) -> c18
   ISCONSTERM(T, F) -> c19
   ISCONSTERM(T, And(z0)) -> c20
   ISCONSTERM(T, Or(z0)) -> c21
   ISCONSTERM(F, T) -> c22
   ISCONSTERM(F, F) -> c23
   ISCONSTERM(F, And(z0)) -> c24
   ISCONSTERM(F, Or(z0)) -> c25
   ISCONSTERM(And(z0), T) -> c26
   ISCONSTERM(And(z0), F) -> c27
   ISCONSTERM(And(z0), And(z2)) -> c28
   ISCONSTERM(And(z0), Or(z2)) -> c29
   ISCONSTERM(Or(z0), T) -> c30
   ISCONSTERM(Or(z0), F) -> c31
   ISCONSTERM(Or(z0), And(z2)) -> c32
   ISCONSTERM(Or(z0), Or(z2)) -> c33
   ISOP(T) -> c34
   ISOP(F) -> c35
   ISOP(And(z0)) -> c36
   ISOP(Or(z0)) -> c37
   ISAND(T) -> c38
   ISAND(F) -> c39
   ISAND(And(z0)) -> c40
   ISAND(Or(z0)) -> c41
   GETSECOND(And(z0)) -> c42
   GETSECOND(Or(z0)) -> c43
   GETFIRST(And(z0)) -> c44
   GETFIRST(Or(z0)) -> 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)) -> conj(And(z0))
   disj(Or(z0)) -> and(conj(z0), disj(z0))
   conj(Or(z0)) -> False
   conj(T) -> True
   conj(F) -> True
   conj(And(z0)) -> and(disj(z0), conj(z0))
   bool(T) -> True
   bool(F) -> True
   bool(And(z0)) -> False
   bool(Or(z0)) -> False
   isConsTerm(T, T) -> True
   isConsTerm(T, F) -> False
   isConsTerm(T, And(z0)) -> False
   isConsTerm(T, Or(z0)) -> False
   isConsTerm(F, T) -> False
   isConsTerm(F, F) -> True
   isConsTerm(F, And(z0)) -> False
   isConsTerm(F, Or(z0)) -> False
   isConsTerm(And(z0), T) -> False
   isConsTerm(And(z0), F) -> False
   isConsTerm(And(z0), And(z2)) -> True
   isConsTerm(And(z0), Or(z2)) -> False
   isConsTerm(Or(z0), T) -> False
   isConsTerm(Or(z0), F) -> False
   isConsTerm(Or(z0), And(z2)) -> False
   isConsTerm(Or(z0), Or(z2)) -> True
   isOp(T) -> False
   isOp(F) -> False
   isOp(And(z0)) -> True
   isOp(Or(z0)) -> True
   isAnd(T) -> False
   isAnd(F) -> False
   isAnd(And(z0)) -> True
   isAnd(Or(z0)) -> False
   getSecond(And(z0)) -> z0
   getSecond(Or(z0)) -> z0
   getFirst(And(z0)) -> z0
   getFirst(Or(z0)) -> z0
   disjconj(z0) -> disj(z0)

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

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
DISJ(T) -> c4
DISJ(F) -> c5
DISJ(And(z0)) -> c6(CONJ(And(z0)))
DISJ(Or(z0)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
DISJ(Or(z0)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
CONJ(Or(z0)) -> c9
CONJ(T) -> c10
CONJ(F) -> c11
CONJ(And(z0)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
CONJ(And(z0)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
BOOL(T) -> c14
BOOL(F) -> c15
BOOL(And(z0)) -> c16
BOOL(Or(z0)) -> c17
ISCONSTERM(T, T) -> c18
ISCONSTERM(T, F) -> c19
ISCONSTERM(T, And(z0)) -> c20
ISCONSTERM(T, Or(z0)) -> c21
ISCONSTERM(F, T) -> c22
ISCONSTERM(F, F) -> c23
ISCONSTERM(F, And(z0)) -> c24
ISCONSTERM(F, Or(z0)) -> c25
ISCONSTERM(And(z0), T) -> c26
ISCONSTERM(And(z0), F) -> c27
ISCONSTERM(And(z0), And(z2)) -> c28
ISCONSTERM(And(z0), Or(z2)) -> c29
ISCONSTERM(Or(z0), T) -> c30
ISCONSTERM(Or(z0), F) -> c31
ISCONSTERM(Or(z0), And(z2)) -> c32
ISCONSTERM(Or(z0), Or(z2)) -> c33
ISOP(T) -> c34
ISOP(F) -> c35
ISOP(And(z0)) -> c36
ISOP(Or(z0)) -> c37
ISAND(T) -> c38
ISAND(F) -> c39
ISAND(And(z0)) -> c40
ISAND(Or(z0)) -> c41
GETSECOND(And(z0)) -> c42
GETSECOND(Or(z0)) -> c43
GETFIRST(And(z0)) -> c44
GETFIRST(Or(z0)) -> 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)) -> conj(And(z0))
disj(Or(z0)) -> and(conj(z0), disj(z0))
conj(Or(z0)) -> False
conj(T) -> True
conj(F) -> True
conj(And(z0)) -> and(disj(z0), conj(z0))
bool(T) -> True
bool(F) -> True
bool(And(z0)) -> False
bool(Or(z0)) -> False
isConsTerm(T, T) -> True
isConsTerm(T, F) -> False
isConsTerm(T, And(z0)) -> False
isConsTerm(T, Or(z0)) -> False
isConsTerm(F, T) -> False
isConsTerm(F, F) -> True
isConsTerm(F, And(z0)) -> False
isConsTerm(F, Or(z0)) -> False
isConsTerm(And(z0), T) -> False
isConsTerm(And(z0), F) -> False
isConsTerm(And(z0), And(z2)) -> True
isConsTerm(And(z0), Or(z2)) -> False
isConsTerm(Or(z0), T) -> False
isConsTerm(Or(z0), F) -> False
isConsTerm(Or(z0), And(z2)) -> False
isConsTerm(Or(z0), Or(z2)) -> True
isOp(T) -> False
isOp(F) -> False
isOp(And(z0)) -> True
isOp(Or(z0)) -> True
isAnd(T) -> False
isAnd(F) -> False
isAnd(And(z0)) -> True
isAnd(Or(z0)) -> False
getSecond(And(z0)) -> z0
getSecond(Or(z0)) -> z0
getFirst(And(z0)) -> z0
getFirst(Or(z0)) -> 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 -> 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 -> 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_c9:c10:c11:c12:c133_47 :: c9:c10:c11:c12:c13
hole_c:c1:c2:c34_47 :: c:c1:c2:c3
hole_False:True5_47 :: False:True
hole_c14:c15:c16:c176_47 :: c14:c15:c16:c17
hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c337_47 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
hole_c34:c35:c36:c378_47 :: c34:c35:c36:c37
hole_c38:c39:c40:c419_47 :: c38:c39:c40:c41
hole_c42:c4310_47 :: c42:c43
hole_c44:c4511_47 :: c44:c45
hole_c4612_47 :: c46
gen_c4:c5:c6:c7:c813_47 :: Nat -> c4:c5:c6:c7:c8
gen_T:F:And:Or14_47 :: Nat -> T:F:And:Or
gen_c9:c10:c11:c12:c1315_47 :: Nat -> c9:c10:c11:c12:c13

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

(9) 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

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

(10)
Obligation:
Innermost TRS:
Rules:
DISJ(T) -> c4
DISJ(F) -> c5
DISJ(And(z0)) -> c6(CONJ(And(z0)))
DISJ(Or(z0)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
DISJ(Or(z0)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
CONJ(Or(z0)) -> c9
CONJ(T) -> c10
CONJ(F) -> c11
CONJ(And(z0)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
CONJ(And(z0)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
BOOL(T) -> c14
BOOL(F) -> c15
BOOL(And(z0)) -> c16
BOOL(Or(z0)) -> c17
ISCONSTERM(T, T) -> c18
ISCONSTERM(T, F) -> c19
ISCONSTERM(T, And(z0)) -> c20
ISCONSTERM(T, Or(z0)) -> c21
ISCONSTERM(F, T) -> c22
ISCONSTERM(F, F) -> c23
ISCONSTERM(F, And(z0)) -> c24
ISCONSTERM(F, Or(z0)) -> c25
ISCONSTERM(And(z0), T) -> c26
ISCONSTERM(And(z0), F) -> c27
ISCONSTERM(And(z0), And(z2)) -> c28
ISCONSTERM(And(z0), Or(z2)) -> c29
ISCONSTERM(Or(z0), T) -> c30
ISCONSTERM(Or(z0), F) -> c31
ISCONSTERM(Or(z0), And(z2)) -> c32
ISCONSTERM(Or(z0), Or(z2)) -> c33
ISOP(T) -> c34
ISOP(F) -> c35
ISOP(And(z0)) -> c36
ISOP(Or(z0)) -> c37
ISAND(T) -> c38
ISAND(F) -> c39
ISAND(And(z0)) -> c40
ISAND(Or(z0)) -> c41
GETSECOND(And(z0)) -> c42
GETSECOND(Or(z0)) -> c43
GETFIRST(And(z0)) -> c44
GETFIRST(Or(z0)) -> 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)) -> conj(And(z0))
disj(Or(z0)) -> and(conj(z0), disj(z0))
conj(Or(z0)) -> False
conj(T) -> True
conj(F) -> True
conj(And(z0)) -> and(disj(z0), conj(z0))
bool(T) -> True
bool(F) -> True
bool(And(z0)) -> False
bool(Or(z0)) -> False
isConsTerm(T, T) -> True
isConsTerm(T, F) -> False
isConsTerm(T, And(z0)) -> False
isConsTerm(T, Or(z0)) -> False
isConsTerm(F, T) -> False
isConsTerm(F, F) -> True
isConsTerm(F, And(z0)) -> False
isConsTerm(F, Or(z0)) -> False
isConsTerm(And(z0), T) -> False
isConsTerm(And(z0), F) -> False
isConsTerm(And(z0), And(z2)) -> True
isConsTerm(And(z0), Or(z2)) -> False
isConsTerm(Or(z0), T) -> False
isConsTerm(Or(z0), F) -> False
isConsTerm(Or(z0), And(z2)) -> False
isConsTerm(Or(z0), Or(z2)) -> True
isOp(T) -> False
isOp(F) -> False
isOp(And(z0)) -> True
isOp(Or(z0)) -> True
isAnd(T) -> False
isAnd(F) -> False
isAnd(And(z0)) -> True
isAnd(Or(z0)) -> False
getSecond(And(z0)) -> z0
getSecond(Or(z0)) -> z0
getFirst(And(z0)) -> z0
getFirst(Or(z0)) -> 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 -> 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 -> 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_c9:c10:c11:c12:c133_47 :: c9:c10:c11:c12:c13
hole_c:c1:c2:c34_47 :: c:c1:c2:c3
hole_False:True5_47 :: False:True
hole_c14:c15:c16:c176_47 :: c14:c15:c16:c17
hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c337_47 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
hole_c34:c35:c36:c378_47 :: c34:c35:c36:c37
hole_c38:c39:c40:c419_47 :: c38:c39:c40:c41
hole_c42:c4310_47 :: c42:c43
hole_c44:c4511_47 :: c44:c45
hole_c4612_47 :: c46
gen_c4:c5:c6:c7:c813_47 :: Nat -> c4:c5:c6:c7:c8
gen_T:F:And:Or14_47 :: Nat -> T:F:And:Or
gen_c9:c10:c11:c12:c1315_47 :: Nat -> c9:c10:c11:c12:c13


Generator Equations:
gen_c4:c5:c6:c7:c813_47(0) <=> c4
gen_c4:c5:c6:c7:c813_47(+(x, 1)) <=> c8(c, gen_c4:c5:c6:c7:c813_47(x))
gen_T:F:And:Or14_47(0) <=> T
gen_T:F:And:Or14_47(+(x, 1)) <=> And(gen_T:F:And:Or14_47(x))
gen_c9:c10:c11:c12:c1315_47(0) <=> c9
gen_c9:c10:c11:c12:c1315_47(+(x, 1)) <=> c13(c, gen_c9:c10:c11:c12:c1315_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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
disj(gen_T:F:And:Or14_47(n17_47)) -> *16_47, rt in Omega(0)

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

Induction Step:
disj(gen_T:F:And:Or14_47(+(n17_47, 1))) ->_R^Omega(0)
conj(And(gen_T:F:And:Or14_47(n17_47))) ->_R^Omega(0)
and(disj(gen_T:F:And:Or14_47(n17_47)), conj(gen_T:F:And:Or14_47(n17_47))) ->_IH
and(*16_47, conj(gen_T:F:And:Or14_47(n17_47)))

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:
DISJ(T) -> c4
DISJ(F) -> c5
DISJ(And(z0)) -> c6(CONJ(And(z0)))
DISJ(Or(z0)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0))
DISJ(Or(z0)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0))
CONJ(Or(z0)) -> c9
CONJ(T) -> c10
CONJ(F) -> c11
CONJ(And(z0)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0))
CONJ(And(z0)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0))
BOOL(T) -> c14
BOOL(F) -> c15
BOOL(And(z0)) -> c16
BOOL(Or(z0)) -> c17
ISCONSTERM(T, T) -> c18
ISCONSTERM(T, F) -> c19
ISCONSTERM(T, And(z0)) -> c20
ISCONSTERM(T, Or(z0)) -> c21
ISCONSTERM(F, T) -> c22
ISCONSTERM(F, F) -> c23
ISCONSTERM(F, And(z0)) -> c24
ISCONSTERM(F, Or(z0)) -> c25
ISCONSTERM(And(z0), T) -> c26
ISCONSTERM(And(z0), F) -> c27
ISCONSTERM(And(z0), And(z2)) -> c28
ISCONSTERM(And(z0), Or(z2)) -> c29
ISCONSTERM(Or(z0), T) -> c30
ISCONSTERM(Or(z0), F) -> c31
ISCONSTERM(Or(z0), And(z2)) -> c32
ISCONSTERM(Or(z0), Or(z2)) -> c33
ISOP(T) -> c34
ISOP(F) -> c35
ISOP(And(z0)) -> c36
ISOP(Or(z0)) -> c37
ISAND(T) -> c38
ISAND(F) -> c39
ISAND(And(z0)) -> c40
ISAND(Or(z0)) -> c41
GETSECOND(And(z0)) -> c42
GETSECOND(Or(z0)) -> c43
GETFIRST(And(z0)) -> c44
GETFIRST(Or(z0)) -> 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)) -> conj(And(z0))
disj(Or(z0)) -> and(conj(z0), disj(z0))
conj(Or(z0)) -> False
conj(T) -> True
conj(F) -> True
conj(And(z0)) -> and(disj(z0), conj(z0))
bool(T) -> True
bool(F) -> True
bool(And(z0)) -> False
bool(Or(z0)) -> False
isConsTerm(T, T) -> True
isConsTerm(T, F) -> False
isConsTerm(T, And(z0)) -> False
isConsTerm(T, Or(z0)) -> False
isConsTerm(F, T) -> False
isConsTerm(F, F) -> True
isConsTerm(F, And(z0)) -> False
isConsTerm(F, Or(z0)) -> False
isConsTerm(And(z0), T) -> False
isConsTerm(And(z0), F) -> False
isConsTerm(And(z0), And(z2)) -> True
isConsTerm(And(z0), Or(z2)) -> False
isConsTerm(Or(z0), T) -> False
isConsTerm(Or(z0), F) -> False
isConsTerm(Or(z0), And(z2)) -> False
isConsTerm(Or(z0), Or(z2)) -> True
isOp(T) -> False
isOp(F) -> False
isOp(And(z0)) -> True
isOp(Or(z0)) -> True
isAnd(T) -> False
isAnd(F) -> False
isAnd(And(z0)) -> True
isAnd(Or(z0)) -> False
getSecond(And(z0)) -> z0
getSecond(Or(z0)) -> z0
getFirst(And(z0)) -> z0
getFirst(Or(z0)) -> 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 -> 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 -> 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_c9:c10:c11:c12:c133_47 :: c9:c10:c11:c12:c13
hole_c:c1:c2:c34_47 :: c:c1:c2:c3
hole_False:True5_47 :: False:True
hole_c14:c15:c16:c176_47 :: c14:c15:c16:c17
hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c337_47 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33
hole_c34:c35:c36:c378_47 :: c34:c35:c36:c37
hole_c38:c39:c40:c419_47 :: c38:c39:c40:c41
hole_c42:c4310_47 :: c42:c43
hole_c44:c4511_47 :: c44:c45
hole_c4612_47 :: c46
gen_c4:c5:c6:c7:c813_47 :: Nat -> c4:c5:c6:c7:c8
gen_T:F:And:Or14_47 :: Nat -> T:F:And:Or
gen_c9:c10:c11:c12:c1315_47 :: Nat -> c9:c10:c11:c12:c13


Lemmas:
disj(gen_T:F:And:Or14_47(n17_47)) -> *16_47, rt in Omega(0)


Generator Equations:
gen_c4:c5:c6:c7:c813_47(0) <=> c4
gen_c4:c5:c6:c7:c813_47(+(x, 1)) <=> c8(c, gen_c4:c5:c6:c7:c813_47(x))
gen_T:F:And:Or14_47(0) <=> T
gen_T:F:And:Or14_47(+(x, 1)) <=> And(gen_T:F:And:Or14_47(x))
gen_c9:c10:c11:c12:c1315_47(0) <=> c9
gen_c9:c10:c11:c12:c1315_47(+(x, 1)) <=> c13(c, gen_c9:c10:c11:c12:c1315_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

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

(13) RewriteLemmaProof (FINISHED)
Proved the following rewrite lemma:
conj(gen_T:F:And:Or14_47(+(1, n9737_47))) -> *16_47, rt in Omega(EXP)

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

Induction Step:
conj(gen_T:F:And:Or14_47(+(1, +(n9737_47, 1)))) ->_R^Omega(0)
and(disj(gen_T:F:And:Or14_47(+(1, n9737_47))), conj(gen_T:F:And:Or14_47(+(1, n9737_47)))) ->_R^Omega(0)
and(conj(And(gen_T:F:And:Or14_47(n9737_47))), conj(gen_T:F:And:Or14_47(+(1, n9737_47)))) ->_IH
and(*16_47, conj(gen_T:F:And:Or14_47(+(1, n9737_47)))) ->_IH
and(*16_47, *16_47)

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

(14)
BOUNDS(EXP, INF)