Runtime Complexity TRS:
The TRS R consists of the following rules:

intersect'ii'in(cons(X, X0), cons(X, X1)) → intersect'ii'out
intersect'ii'in(Xs, cons(X0, Ys)) → u'1'1(intersect'ii'in(Xs, Ys))
u'1'1(intersect'ii'out) → intersect'ii'out
intersect'ii'in(cons(X0, Xs), Ys) → u'2'1(intersect'ii'in(Xs, Ys))
u'2'1(intersect'ii'out) → intersect'ii'out
reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) → u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF))
u'3'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) → u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF))
u'4'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) → u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF))
u'5'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) → u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1(reduce'ii'out, F2, Fs, Gs, NF) → u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))
u'6'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) → u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))
u'7'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) → u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF))
u'8'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) → u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF))
u'9'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) → u'10'1(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)))
u'10'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) → u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF))
u'11'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) → u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1(reduce'ii'out, Fs, G2, Gs, NF) → u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))
u'12'2(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) → u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))
u'13'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, cons(p(V), Gs)), sequent(Left, Right)) → u'14'1(reduce'ii'in(sequent(nil, Gs), sequent(Left, cons(p(V), Right))))
u'14'1(reduce'ii'out) → reduce'ii'out
reduce'ii'in(sequent(nil, nil), sequent(F1, F2)) → u'15'1(intersect'ii'in(F1, F2))
u'15'1(intersect'ii'out) → reduce'ii'out
tautology'i'in(F) → u'16'1(reduce'ii'in(sequent(nil, cons(F, nil)), sequent(nil, nil)))
u'16'1(reduce'ii'out) → tautology'i'out

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


intersect'ii'in'(cons'(X, X0), cons'(X, X1)) → intersect'ii'out'
intersect'ii'in'(Xs, cons'(X0, Ys)) → u'1'1'(intersect'ii'in'(Xs, Ys))
u'1'1'(intersect'ii'out') → intersect'ii'out'
intersect'ii'in'(cons'(X0, Xs), Ys) → u'2'1'(intersect'ii'in'(Xs, Ys))
u'2'1'(intersect'ii'out') → intersect'ii'out'
reduce'ii'in'(sequent'(cons'(if'(A, B), Fs), Gs), NF) → u'3'1'(reduce'ii'in'(sequent'(cons'(x'2b'(x'2d'(B), A), Fs), Gs), NF))
u'3'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(iff'(A, B), Fs), Gs), NF) → u'4'1'(reduce'ii'in'(sequent'(cons'(x'2a'(if'(A, B), if'(B, A)), Fs), Gs), NF))
u'4'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2a'(F1, F2), Fs), Gs), NF) → u'5'1'(reduce'ii'in'(sequent'(cons'(F1, cons'(F2, Fs)), Gs), NF))
u'5'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2b'(F1, F2), Fs), Gs), NF) → u'6'1'(reduce'ii'in'(sequent'(cons'(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1'(reduce'ii'out', F2, Fs, Gs, NF) → u'6'2'(reduce'ii'in'(sequent'(cons'(F2, Fs), Gs), NF))
u'6'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2d'(F1), Fs), Gs), NF) → u'7'1'(reduce'ii'in'(sequent'(Fs, cons'(F1, Gs)), NF))
u'7'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(if'(A, B), Gs)), NF) → u'8'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2b'(x'2d'(B), A), Gs)), NF))
u'8'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(iff'(A, B), Gs)), NF) → u'9'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2a'(if'(A, B), if'(B, A)), Gs)), NF))
u'9'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(p'(V), Fs), Gs), sequent'(Left, Right)) → u'10'1'(reduce'ii'in'(sequent'(Fs, Gs), sequent'(cons'(p'(V), Left), Right)))
u'10'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2b'(G1, G2), Gs)), NF) → u'11'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, cons'(G2, Gs))), NF))
u'11'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2a'(G1, G2), Gs)), NF) → u'12'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1'(reduce'ii'out', Fs, G2, Gs, NF) → u'12'2'(reduce'ii'in'(sequent'(Fs, cons'(G2, Gs)), NF))
u'12'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2d'(G1), Gs)), NF) → u'13'1'(reduce'ii'in'(sequent'(cons'(G1, Fs), Gs), NF))
u'13'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', cons'(p'(V), Gs)), sequent'(Left, Right)) → u'14'1'(reduce'ii'in'(sequent'(nil', Gs), sequent'(Left, cons'(p'(V), Right))))
u'14'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', nil'), sequent'(F1, F2)) → u'15'1'(intersect'ii'in'(F1, F2))
u'15'1'(intersect'ii'out') → reduce'ii'out'
tautology'i'in'(F) → u'16'1'(reduce'ii'in'(sequent'(nil', cons'(F, nil')), sequent'(nil', nil')))
u'16'1'(reduce'ii'out') → tautology'i'out'

Rewrite Strategy: INNERMOST

Sliced the following arguments:
p'/0

Runtime Complexity TRS:
The TRS R consists of the following rules:


intersect'ii'in'(cons'(X, X0), cons'(X, X1)) → intersect'ii'out'
intersect'ii'in'(Xs, cons'(X0, Ys)) → u'1'1'(intersect'ii'in'(Xs, Ys))
u'1'1'(intersect'ii'out') → intersect'ii'out'
intersect'ii'in'(cons'(X0, Xs), Ys) → u'2'1'(intersect'ii'in'(Xs, Ys))
u'2'1'(intersect'ii'out') → intersect'ii'out'
reduce'ii'in'(sequent'(cons'(if'(A, B), Fs), Gs), NF) → u'3'1'(reduce'ii'in'(sequent'(cons'(x'2b'(x'2d'(B), A), Fs), Gs), NF))
u'3'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(iff'(A, B), Fs), Gs), NF) → u'4'1'(reduce'ii'in'(sequent'(cons'(x'2a'(if'(A, B), if'(B, A)), Fs), Gs), NF))
u'4'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2a'(F1, F2), Fs), Gs), NF) → u'5'1'(reduce'ii'in'(sequent'(cons'(F1, cons'(F2, Fs)), Gs), NF))
u'5'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2b'(F1, F2), Fs), Gs), NF) → u'6'1'(reduce'ii'in'(sequent'(cons'(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1'(reduce'ii'out', F2, Fs, Gs, NF) → u'6'2'(reduce'ii'in'(sequent'(cons'(F2, Fs), Gs), NF))
u'6'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2d'(F1), Fs), Gs), NF) → u'7'1'(reduce'ii'in'(sequent'(Fs, cons'(F1, Gs)), NF))
u'7'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(if'(A, B), Gs)), NF) → u'8'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2b'(x'2d'(B), A), Gs)), NF))
u'8'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(iff'(A, B), Gs)), NF) → u'9'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2a'(if'(A, B), if'(B, A)), Gs)), NF))
u'9'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(p', Fs), Gs), sequent'(Left, Right)) → u'10'1'(reduce'ii'in'(sequent'(Fs, Gs), sequent'(cons'(p', Left), Right)))
u'10'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2b'(G1, G2), Gs)), NF) → u'11'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, cons'(G2, Gs))), NF))
u'11'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2a'(G1, G2), Gs)), NF) → u'12'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1'(reduce'ii'out', Fs, G2, Gs, NF) → u'12'2'(reduce'ii'in'(sequent'(Fs, cons'(G2, Gs)), NF))
u'12'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2d'(G1), Gs)), NF) → u'13'1'(reduce'ii'in'(sequent'(cons'(G1, Fs), Gs), NF))
u'13'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', cons'(p', Gs)), sequent'(Left, Right)) → u'14'1'(reduce'ii'in'(sequent'(nil', Gs), sequent'(Left, cons'(p', Right))))
u'14'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', nil'), sequent'(F1, F2)) → u'15'1'(intersect'ii'in'(F1, F2))
u'15'1'(intersect'ii'out') → reduce'ii'out'
tautology'i'in'(F) → u'16'1'(reduce'ii'in'(sequent'(nil', cons'(F, nil')), sequent'(nil', nil')))
u'16'1'(reduce'ii'out') → tautology'i'out'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
intersect'ii'in'(cons'(X, X0), cons'(X, X1)) → intersect'ii'out'
intersect'ii'in'(Xs, cons'(X0, Ys)) → u'1'1'(intersect'ii'in'(Xs, Ys))
u'1'1'(intersect'ii'out') → intersect'ii'out'
intersect'ii'in'(cons'(X0, Xs), Ys) → u'2'1'(intersect'ii'in'(Xs, Ys))
u'2'1'(intersect'ii'out') → intersect'ii'out'
reduce'ii'in'(sequent'(cons'(if'(A, B), Fs), Gs), NF) → u'3'1'(reduce'ii'in'(sequent'(cons'(x'2b'(x'2d'(B), A), Fs), Gs), NF))
u'3'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(iff'(A, B), Fs), Gs), NF) → u'4'1'(reduce'ii'in'(sequent'(cons'(x'2a'(if'(A, B), if'(B, A)), Fs), Gs), NF))
u'4'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2a'(F1, F2), Fs), Gs), NF) → u'5'1'(reduce'ii'in'(sequent'(cons'(F1, cons'(F2, Fs)), Gs), NF))
u'5'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2b'(F1, F2), Fs), Gs), NF) → u'6'1'(reduce'ii'in'(sequent'(cons'(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1'(reduce'ii'out', F2, Fs, Gs, NF) → u'6'2'(reduce'ii'in'(sequent'(cons'(F2, Fs), Gs), NF))
u'6'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2d'(F1), Fs), Gs), NF) → u'7'1'(reduce'ii'in'(sequent'(Fs, cons'(F1, Gs)), NF))
u'7'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(if'(A, B), Gs)), NF) → u'8'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2b'(x'2d'(B), A), Gs)), NF))
u'8'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(iff'(A, B), Gs)), NF) → u'9'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2a'(if'(A, B), if'(B, A)), Gs)), NF))
u'9'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(p', Fs), Gs), sequent'(Left, Right)) → u'10'1'(reduce'ii'in'(sequent'(Fs, Gs), sequent'(cons'(p', Left), Right)))
u'10'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2b'(G1, G2), Gs)), NF) → u'11'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, cons'(G2, Gs))), NF))
u'11'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2a'(G1, G2), Gs)), NF) → u'12'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1'(reduce'ii'out', Fs, G2, Gs, NF) → u'12'2'(reduce'ii'in'(sequent'(Fs, cons'(G2, Gs)), NF))
u'12'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2d'(G1), Gs)), NF) → u'13'1'(reduce'ii'in'(sequent'(cons'(G1, Fs), Gs), NF))
u'13'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', cons'(p', Gs)), sequent'(Left, Right)) → u'14'1'(reduce'ii'in'(sequent'(nil', Gs), sequent'(Left, cons'(p', Right))))
u'14'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', nil'), sequent'(F1, F2)) → u'15'1'(intersect'ii'in'(F1, F2))
u'15'1'(intersect'ii'out') → reduce'ii'out'
tautology'i'in'(F) → u'16'1'(reduce'ii'in'(sequent'(nil', cons'(F, nil')), sequent'(nil', nil')))
u'16'1'(reduce'ii'out') → tautology'i'out'

Types:
intersect'ii'in' :: cons':nil' → cons':nil' → intersect'ii'out'
cons' :: if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil'
intersect'ii'out' :: intersect'ii'out'
u'1'1' :: intersect'ii'out' → intersect'ii'out'
u'2'1' :: intersect'ii'out' → intersect'ii'out'
reduce'ii'in' :: sequent' → sequent' → reduce'ii'out'
sequent' :: cons':nil' → cons':nil' → sequent'
if' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'3'1' :: reduce'ii'out' → reduce'ii'out'
x'2b' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
x'2d' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
reduce'ii'out' :: reduce'ii'out'
iff' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'4'1' :: reduce'ii'out' → reduce'ii'out'
x'2a' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'5'1' :: reduce'ii'out' → reduce'ii'out'
u'6'1' :: reduce'ii'out' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil' → sequent' → reduce'ii'out'
u'6'2' :: reduce'ii'out' → reduce'ii'out'
u'7'1' :: reduce'ii'out' → reduce'ii'out'
u'8'1' :: reduce'ii'out' → reduce'ii'out'
u'9'1' :: reduce'ii'out' → reduce'ii'out'
p' :: if':x'2d':x'2b':iff':x'2a':p'
u'10'1' :: reduce'ii'out' → reduce'ii'out'
u'11'1' :: reduce'ii'out' → reduce'ii'out'
u'12'1' :: reduce'ii'out' → cons':nil' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → sequent' → reduce'ii'out'
u'12'2' :: reduce'ii'out' → reduce'ii'out'
u'13'1' :: reduce'ii'out' → reduce'ii'out'
nil' :: cons':nil'
u'14'1' :: reduce'ii'out' → reduce'ii'out'
u'15'1' :: intersect'ii'out' → reduce'ii'out'
tautology'i'in' :: if':x'2d':x'2b':iff':x'2a':p' → tautology'i'out'
u'16'1' :: reduce'ii'out' → tautology'i'out'
tautology'i'out' :: tautology'i'out'
_hole_intersect'ii'out'1 :: intersect'ii'out'
_hole_cons':nil'2 :: cons':nil'
_hole_if':x'2d':x'2b':iff':x'2a':p'3 :: if':x'2d':x'2b':iff':x'2a':p'
_hole_reduce'ii'out'4 :: reduce'ii'out'
_hole_sequent'5 :: sequent'
_hole_tautology'i'out'6 :: tautology'i'out'
_gen_cons':nil'7 :: Nat → cons':nil'
_gen_if':x'2d':x'2b':iff':x'2a':p'8 :: Nat → if':x'2d':x'2b':iff':x'2a':p'

Heuristically decided to analyse the following defined symbols:
intersect'ii'in', reduce'ii'in'

They will be analysed ascendingly in the following order:
intersect'ii'in' < reduce'ii'in'

Rules:
intersect'ii'in'(cons'(X, X0), cons'(X, X1)) → intersect'ii'out'
intersect'ii'in'(Xs, cons'(X0, Ys)) → u'1'1'(intersect'ii'in'(Xs, Ys))
u'1'1'(intersect'ii'out') → intersect'ii'out'
intersect'ii'in'(cons'(X0, Xs), Ys) → u'2'1'(intersect'ii'in'(Xs, Ys))
u'2'1'(intersect'ii'out') → intersect'ii'out'
reduce'ii'in'(sequent'(cons'(if'(A, B), Fs), Gs), NF) → u'3'1'(reduce'ii'in'(sequent'(cons'(x'2b'(x'2d'(B), A), Fs), Gs), NF))
u'3'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(iff'(A, B), Fs), Gs), NF) → u'4'1'(reduce'ii'in'(sequent'(cons'(x'2a'(if'(A, B), if'(B, A)), Fs), Gs), NF))
u'4'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2a'(F1, F2), Fs), Gs), NF) → u'5'1'(reduce'ii'in'(sequent'(cons'(F1, cons'(F2, Fs)), Gs), NF))
u'5'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2b'(F1, F2), Fs), Gs), NF) → u'6'1'(reduce'ii'in'(sequent'(cons'(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1'(reduce'ii'out', F2, Fs, Gs, NF) → u'6'2'(reduce'ii'in'(sequent'(cons'(F2, Fs), Gs), NF))
u'6'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2d'(F1), Fs), Gs), NF) → u'7'1'(reduce'ii'in'(sequent'(Fs, cons'(F1, Gs)), NF))
u'7'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(if'(A, B), Gs)), NF) → u'8'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2b'(x'2d'(B), A), Gs)), NF))
u'8'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(iff'(A, B), Gs)), NF) → u'9'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2a'(if'(A, B), if'(B, A)), Gs)), NF))
u'9'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(p', Fs), Gs), sequent'(Left, Right)) → u'10'1'(reduce'ii'in'(sequent'(Fs, Gs), sequent'(cons'(p', Left), Right)))
u'10'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2b'(G1, G2), Gs)), NF) → u'11'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, cons'(G2, Gs))), NF))
u'11'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2a'(G1, G2), Gs)), NF) → u'12'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1'(reduce'ii'out', Fs, G2, Gs, NF) → u'12'2'(reduce'ii'in'(sequent'(Fs, cons'(G2, Gs)), NF))
u'12'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2d'(G1), Gs)), NF) → u'13'1'(reduce'ii'in'(sequent'(cons'(G1, Fs), Gs), NF))
u'13'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', cons'(p', Gs)), sequent'(Left, Right)) → u'14'1'(reduce'ii'in'(sequent'(nil', Gs), sequent'(Left, cons'(p', Right))))
u'14'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', nil'), sequent'(F1, F2)) → u'15'1'(intersect'ii'in'(F1, F2))
u'15'1'(intersect'ii'out') → reduce'ii'out'
tautology'i'in'(F) → u'16'1'(reduce'ii'in'(sequent'(nil', cons'(F, nil')), sequent'(nil', nil')))
u'16'1'(reduce'ii'out') → tautology'i'out'

Types:
intersect'ii'in' :: cons':nil' → cons':nil' → intersect'ii'out'
cons' :: if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil'
intersect'ii'out' :: intersect'ii'out'
u'1'1' :: intersect'ii'out' → intersect'ii'out'
u'2'1' :: intersect'ii'out' → intersect'ii'out'
reduce'ii'in' :: sequent' → sequent' → reduce'ii'out'
sequent' :: cons':nil' → cons':nil' → sequent'
if' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'3'1' :: reduce'ii'out' → reduce'ii'out'
x'2b' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
x'2d' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
reduce'ii'out' :: reduce'ii'out'
iff' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'4'1' :: reduce'ii'out' → reduce'ii'out'
x'2a' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'5'1' :: reduce'ii'out' → reduce'ii'out'
u'6'1' :: reduce'ii'out' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil' → sequent' → reduce'ii'out'
u'6'2' :: reduce'ii'out' → reduce'ii'out'
u'7'1' :: reduce'ii'out' → reduce'ii'out'
u'8'1' :: reduce'ii'out' → reduce'ii'out'
u'9'1' :: reduce'ii'out' → reduce'ii'out'
p' :: if':x'2d':x'2b':iff':x'2a':p'
u'10'1' :: reduce'ii'out' → reduce'ii'out'
u'11'1' :: reduce'ii'out' → reduce'ii'out'
u'12'1' :: reduce'ii'out' → cons':nil' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → sequent' → reduce'ii'out'
u'12'2' :: reduce'ii'out' → reduce'ii'out'
u'13'1' :: reduce'ii'out' → reduce'ii'out'
nil' :: cons':nil'
u'14'1' :: reduce'ii'out' → reduce'ii'out'
u'15'1' :: intersect'ii'out' → reduce'ii'out'
tautology'i'in' :: if':x'2d':x'2b':iff':x'2a':p' → tautology'i'out'
u'16'1' :: reduce'ii'out' → tautology'i'out'
tautology'i'out' :: tautology'i'out'
_hole_intersect'ii'out'1 :: intersect'ii'out'
_hole_cons':nil'2 :: cons':nil'
_hole_if':x'2d':x'2b':iff':x'2a':p'3 :: if':x'2d':x'2b':iff':x'2a':p'
_hole_reduce'ii'out'4 :: reduce'ii'out'
_hole_sequent'5 :: sequent'
_hole_tautology'i'out'6 :: tautology'i'out'
_gen_cons':nil'7 :: Nat → cons':nil'
_gen_if':x'2d':x'2b':iff':x'2a':p'8 :: Nat → if':x'2d':x'2b':iff':x'2a':p'

Generator Equations:
_gen_cons':nil'7(0) ⇔ nil'
_gen_cons':nil'7(+(x, 1)) ⇔ cons'(p', _gen_cons':nil'7(x))
_gen_if':x'2d':x'2b':iff':x'2a':p'8(0) ⇔ p'
_gen_if':x'2d':x'2b':iff':x'2a':p'8(+(x, 1)) ⇔ if'(p', _gen_if':x'2d':x'2b':iff':x'2a':p'8(x))

The following defined symbols remain to be analysed:
intersect'ii'in', reduce'ii'in'

They will be analysed ascendingly in the following order:
intersect'ii'in' < reduce'ii'in'

Proved the following rewrite lemma:
intersect'ii'in'(_gen_cons':nil'7(a), _gen_cons':nil'7(+(1, _n10))) → _*9, rt ∈ Ω(n10)

Induction Base:
intersect'ii'in'(_gen_cons':nil'7(a), _gen_cons':nil'7(+(1, 0)))

Induction Step:
intersect'ii'in'(_gen_cons':nil'7(_a834), _gen_cons':nil'7(+(1, +(_$n11, 1)))) →RΩ(1)
u'1'1'(intersect'ii'in'(_gen_cons':nil'7(_a834), _gen_cons':nil'7(+(1, _$n11)))) →IH
u'1'1'(_*9)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
intersect'ii'in'(cons'(X, X0), cons'(X, X1)) → intersect'ii'out'
intersect'ii'in'(Xs, cons'(X0, Ys)) → u'1'1'(intersect'ii'in'(Xs, Ys))
u'1'1'(intersect'ii'out') → intersect'ii'out'
intersect'ii'in'(cons'(X0, Xs), Ys) → u'2'1'(intersect'ii'in'(Xs, Ys))
u'2'1'(intersect'ii'out') → intersect'ii'out'
reduce'ii'in'(sequent'(cons'(if'(A, B), Fs), Gs), NF) → u'3'1'(reduce'ii'in'(sequent'(cons'(x'2b'(x'2d'(B), A), Fs), Gs), NF))
u'3'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(iff'(A, B), Fs), Gs), NF) → u'4'1'(reduce'ii'in'(sequent'(cons'(x'2a'(if'(A, B), if'(B, A)), Fs), Gs), NF))
u'4'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2a'(F1, F2), Fs), Gs), NF) → u'5'1'(reduce'ii'in'(sequent'(cons'(F1, cons'(F2, Fs)), Gs), NF))
u'5'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2b'(F1, F2), Fs), Gs), NF) → u'6'1'(reduce'ii'in'(sequent'(cons'(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1'(reduce'ii'out', F2, Fs, Gs, NF) → u'6'2'(reduce'ii'in'(sequent'(cons'(F2, Fs), Gs), NF))
u'6'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2d'(F1), Fs), Gs), NF) → u'7'1'(reduce'ii'in'(sequent'(Fs, cons'(F1, Gs)), NF))
u'7'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(if'(A, B), Gs)), NF) → u'8'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2b'(x'2d'(B), A), Gs)), NF))
u'8'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(iff'(A, B), Gs)), NF) → u'9'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2a'(if'(A, B), if'(B, A)), Gs)), NF))
u'9'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(p', Fs), Gs), sequent'(Left, Right)) → u'10'1'(reduce'ii'in'(sequent'(Fs, Gs), sequent'(cons'(p', Left), Right)))
u'10'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2b'(G1, G2), Gs)), NF) → u'11'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, cons'(G2, Gs))), NF))
u'11'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2a'(G1, G2), Gs)), NF) → u'12'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1'(reduce'ii'out', Fs, G2, Gs, NF) → u'12'2'(reduce'ii'in'(sequent'(Fs, cons'(G2, Gs)), NF))
u'12'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2d'(G1), Gs)), NF) → u'13'1'(reduce'ii'in'(sequent'(cons'(G1, Fs), Gs), NF))
u'13'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', cons'(p', Gs)), sequent'(Left, Right)) → u'14'1'(reduce'ii'in'(sequent'(nil', Gs), sequent'(Left, cons'(p', Right))))
u'14'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', nil'), sequent'(F1, F2)) → u'15'1'(intersect'ii'in'(F1, F2))
u'15'1'(intersect'ii'out') → reduce'ii'out'
tautology'i'in'(F) → u'16'1'(reduce'ii'in'(sequent'(nil', cons'(F, nil')), sequent'(nil', nil')))
u'16'1'(reduce'ii'out') → tautology'i'out'

Types:
intersect'ii'in' :: cons':nil' → cons':nil' → intersect'ii'out'
cons' :: if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil'
intersect'ii'out' :: intersect'ii'out'
u'1'1' :: intersect'ii'out' → intersect'ii'out'
u'2'1' :: intersect'ii'out' → intersect'ii'out'
reduce'ii'in' :: sequent' → sequent' → reduce'ii'out'
sequent' :: cons':nil' → cons':nil' → sequent'
if' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'3'1' :: reduce'ii'out' → reduce'ii'out'
x'2b' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
x'2d' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
reduce'ii'out' :: reduce'ii'out'
iff' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'4'1' :: reduce'ii'out' → reduce'ii'out'
x'2a' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'5'1' :: reduce'ii'out' → reduce'ii'out'
u'6'1' :: reduce'ii'out' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil' → sequent' → reduce'ii'out'
u'6'2' :: reduce'ii'out' → reduce'ii'out'
u'7'1' :: reduce'ii'out' → reduce'ii'out'
u'8'1' :: reduce'ii'out' → reduce'ii'out'
u'9'1' :: reduce'ii'out' → reduce'ii'out'
p' :: if':x'2d':x'2b':iff':x'2a':p'
u'10'1' :: reduce'ii'out' → reduce'ii'out'
u'11'1' :: reduce'ii'out' → reduce'ii'out'
u'12'1' :: reduce'ii'out' → cons':nil' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → sequent' → reduce'ii'out'
u'12'2' :: reduce'ii'out' → reduce'ii'out'
u'13'1' :: reduce'ii'out' → reduce'ii'out'
nil' :: cons':nil'
u'14'1' :: reduce'ii'out' → reduce'ii'out'
u'15'1' :: intersect'ii'out' → reduce'ii'out'
tautology'i'in' :: if':x'2d':x'2b':iff':x'2a':p' → tautology'i'out'
u'16'1' :: reduce'ii'out' → tautology'i'out'
tautology'i'out' :: tautology'i'out'
_hole_intersect'ii'out'1 :: intersect'ii'out'
_hole_cons':nil'2 :: cons':nil'
_hole_if':x'2d':x'2b':iff':x'2a':p'3 :: if':x'2d':x'2b':iff':x'2a':p'
_hole_reduce'ii'out'4 :: reduce'ii'out'
_hole_sequent'5 :: sequent'
_hole_tautology'i'out'6 :: tautology'i'out'
_gen_cons':nil'7 :: Nat → cons':nil'
_gen_if':x'2d':x'2b':iff':x'2a':p'8 :: Nat → if':x'2d':x'2b':iff':x'2a':p'

Lemmas:
intersect'ii'in'(_gen_cons':nil'7(a), _gen_cons':nil'7(+(1, _n10))) → _*9, rt ∈ Ω(n10)

Generator Equations:
_gen_cons':nil'7(0) ⇔ nil'
_gen_cons':nil'7(+(x, 1)) ⇔ cons'(p', _gen_cons':nil'7(x))
_gen_if':x'2d':x'2b':iff':x'2a':p'8(0) ⇔ p'
_gen_if':x'2d':x'2b':iff':x'2a':p'8(+(x, 1)) ⇔ if'(p', _gen_if':x'2d':x'2b':iff':x'2a':p'8(x))

The following defined symbols remain to be analysed:
reduce'ii'in'

Could not prove a rewrite lemma for the defined symbol reduce'ii'in'.

Rules:
intersect'ii'in'(cons'(X, X0), cons'(X, X1)) → intersect'ii'out'
intersect'ii'in'(Xs, cons'(X0, Ys)) → u'1'1'(intersect'ii'in'(Xs, Ys))
u'1'1'(intersect'ii'out') → intersect'ii'out'
intersect'ii'in'(cons'(X0, Xs), Ys) → u'2'1'(intersect'ii'in'(Xs, Ys))
u'2'1'(intersect'ii'out') → intersect'ii'out'
reduce'ii'in'(sequent'(cons'(if'(A, B), Fs), Gs), NF) → u'3'1'(reduce'ii'in'(sequent'(cons'(x'2b'(x'2d'(B), A), Fs), Gs), NF))
u'3'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(iff'(A, B), Fs), Gs), NF) → u'4'1'(reduce'ii'in'(sequent'(cons'(x'2a'(if'(A, B), if'(B, A)), Fs), Gs), NF))
u'4'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2a'(F1, F2), Fs), Gs), NF) → u'5'1'(reduce'ii'in'(sequent'(cons'(F1, cons'(F2, Fs)), Gs), NF))
u'5'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2b'(F1, F2), Fs), Gs), NF) → u'6'1'(reduce'ii'in'(sequent'(cons'(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1'(reduce'ii'out', F2, Fs, Gs, NF) → u'6'2'(reduce'ii'in'(sequent'(cons'(F2, Fs), Gs), NF))
u'6'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(x'2d'(F1), Fs), Gs), NF) → u'7'1'(reduce'ii'in'(sequent'(Fs, cons'(F1, Gs)), NF))
u'7'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(if'(A, B), Gs)), NF) → u'8'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2b'(x'2d'(B), A), Gs)), NF))
u'8'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(iff'(A, B), Gs)), NF) → u'9'1'(reduce'ii'in'(sequent'(Fs, cons'(x'2a'(if'(A, B), if'(B, A)), Gs)), NF))
u'9'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(cons'(p', Fs), Gs), sequent'(Left, Right)) → u'10'1'(reduce'ii'in'(sequent'(Fs, Gs), sequent'(cons'(p', Left), Right)))
u'10'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2b'(G1, G2), Gs)), NF) → u'11'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, cons'(G2, Gs))), NF))
u'11'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2a'(G1, G2), Gs)), NF) → u'12'1'(reduce'ii'in'(sequent'(Fs, cons'(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1'(reduce'ii'out', Fs, G2, Gs, NF) → u'12'2'(reduce'ii'in'(sequent'(Fs, cons'(G2, Gs)), NF))
u'12'2'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(Fs, cons'(x'2d'(G1), Gs)), NF) → u'13'1'(reduce'ii'in'(sequent'(cons'(G1, Fs), Gs), NF))
u'13'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', cons'(p', Gs)), sequent'(Left, Right)) → u'14'1'(reduce'ii'in'(sequent'(nil', Gs), sequent'(Left, cons'(p', Right))))
u'14'1'(reduce'ii'out') → reduce'ii'out'
reduce'ii'in'(sequent'(nil', nil'), sequent'(F1, F2)) → u'15'1'(intersect'ii'in'(F1, F2))
u'15'1'(intersect'ii'out') → reduce'ii'out'
tautology'i'in'(F) → u'16'1'(reduce'ii'in'(sequent'(nil', cons'(F, nil')), sequent'(nil', nil')))
u'16'1'(reduce'ii'out') → tautology'i'out'

Types:
intersect'ii'in' :: cons':nil' → cons':nil' → intersect'ii'out'
cons' :: if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil'
intersect'ii'out' :: intersect'ii'out'
u'1'1' :: intersect'ii'out' → intersect'ii'out'
u'2'1' :: intersect'ii'out' → intersect'ii'out'
reduce'ii'in' :: sequent' → sequent' → reduce'ii'out'
sequent' :: cons':nil' → cons':nil' → sequent'
if' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'3'1' :: reduce'ii'out' → reduce'ii'out'
x'2b' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
x'2d' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
reduce'ii'out' :: reduce'ii'out'
iff' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'4'1' :: reduce'ii'out' → reduce'ii'out'
x'2a' :: if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p' → if':x'2d':x'2b':iff':x'2a':p'
u'5'1' :: reduce'ii'out' → reduce'ii'out'
u'6'1' :: reduce'ii'out' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → cons':nil' → sequent' → reduce'ii'out'
u'6'2' :: reduce'ii'out' → reduce'ii'out'
u'7'1' :: reduce'ii'out' → reduce'ii'out'
u'8'1' :: reduce'ii'out' → reduce'ii'out'
u'9'1' :: reduce'ii'out' → reduce'ii'out'
p' :: if':x'2d':x'2b':iff':x'2a':p'
u'10'1' :: reduce'ii'out' → reduce'ii'out'
u'11'1' :: reduce'ii'out' → reduce'ii'out'
u'12'1' :: reduce'ii'out' → cons':nil' → if':x'2d':x'2b':iff':x'2a':p' → cons':nil' → sequent' → reduce'ii'out'
u'12'2' :: reduce'ii'out' → reduce'ii'out'
u'13'1' :: reduce'ii'out' → reduce'ii'out'
nil' :: cons':nil'
u'14'1' :: reduce'ii'out' → reduce'ii'out'
u'15'1' :: intersect'ii'out' → reduce'ii'out'
tautology'i'in' :: if':x'2d':x'2b':iff':x'2a':p' → tautology'i'out'
u'16'1' :: reduce'ii'out' → tautology'i'out'
tautology'i'out' :: tautology'i'out'
_hole_intersect'ii'out'1 :: intersect'ii'out'
_hole_cons':nil'2 :: cons':nil'
_hole_if':x'2d':x'2b':iff':x'2a':p'3 :: if':x'2d':x'2b':iff':x'2a':p'
_hole_reduce'ii'out'4 :: reduce'ii'out'
_hole_sequent'5 :: sequent'
_hole_tautology'i'out'6 :: tautology'i'out'
_gen_cons':nil'7 :: Nat → cons':nil'
_gen_if':x'2d':x'2b':iff':x'2a':p'8 :: Nat → if':x'2d':x'2b':iff':x'2a':p'

Lemmas:
intersect'ii'in'(_gen_cons':nil'7(a), _gen_cons':nil'7(+(1, _n10))) → _*9, rt ∈ Ω(n10)

Generator Equations:
_gen_cons':nil'7(0) ⇔ nil'
_gen_cons':nil'7(+(x, 1)) ⇔ cons'(p', _gen_cons':nil'7(x))
_gen_if':x'2d':x'2b':iff':x'2a':p'8(0) ⇔ p'
_gen_if':x'2d':x'2b':iff':x'2a':p'8(+(x, 1)) ⇔ if'(p', _gen_if':x'2d':x'2b':iff':x'2a':p'8(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
intersect'ii'in'(_gen_cons':nil'7(a), _gen_cons':nil'7(+(1, _n10))) → _*9, rt ∈ Ω(n10)