MAYBE TRS: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)), intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out(), intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)), u'1'1(intersect'ii'out()) -> intersect'ii'out(), u'2'1(intersect'ii'out()) -> intersect'ii'out(), u'3'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)), reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), 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)), 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), 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)), 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), reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), 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)), 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)), 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)), 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))), 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)))), reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2)), u'4'1(reduce'ii'out()) -> reduce'ii'out(), u'5'1(reduce'ii'out()) -> reduce'ii'out(), 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(), 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(), u'10'1(reduce'ii'out()) -> reduce'ii'out(), u'11'1(reduce'ii'out()) -> reduce'ii'out(), 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(), u'13'1(reduce'ii'out()) -> reduce'ii'out(), u'14'1(reduce'ii'out()) -> reduce'ii'out(), u'15'1(intersect'ii'out()) -> reduce'ii'out(), u'16'1(reduce'ii'out()) -> tautology'i'out(), tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))} DP: Strict: { intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(Xs, cons(X0, Ys)) -> u'1'1#(intersect'ii'in(Xs, Ys)), intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> u'2'1#(intersect'ii'in(Xs, Ys)), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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)), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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)), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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)), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), 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)), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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)), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), 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)), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), 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)))), reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2), reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1#(intersect'ii'in(F1, F2)), u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(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)), tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), tautology'i'in#(F) -> u'16'1#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))} Weak: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)), intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out(), intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)), u'1'1(intersect'ii'out()) -> intersect'ii'out(), u'2'1(intersect'ii'out()) -> intersect'ii'out(), u'3'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)), reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), 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)), 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), 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)), 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), reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), 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)), 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)), 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)), 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))), 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)))), reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2)), u'4'1(reduce'ii'out()) -> reduce'ii'out(), u'5'1(reduce'ii'out()) -> reduce'ii'out(), 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(), 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(), u'10'1(reduce'ii'out()) -> reduce'ii'out(), u'11'1(reduce'ii'out()) -> reduce'ii'out(), 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(), u'13'1(reduce'ii'out()) -> reduce'ii'out(), u'14'1(reduce'ii'out()) -> reduce'ii'out(), u'15'1(intersect'ii'out()) -> reduce'ii'out(), u'16'1(reduce'ii'out()) -> tautology'i'out(), tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))} EDG: { (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))) (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) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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)))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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)))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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)))) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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)))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), 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))) (reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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)))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), 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'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), 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))))) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), 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))) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), 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)) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), 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))) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), 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))) (tautology'i'in#(F) -> reduce'ii'in#(sequent(nil(), cons(F, nil())), sequent(nil(), nil())), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> u'2'1#(intersect'ii'in(Xs, Ys))) (intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys)) (intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(Xs, cons(X0, Ys)) -> u'1'1#(intersect'ii'in(Xs, Ys))) (intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1#(intersect'ii'in(F1, F2))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), 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))))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), 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))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), 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)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), 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))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), 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))) (reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys)) (intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(Xs, cons(X0, Ys)) -> u'1'1#(intersect'ii'in(Xs, Ys))) (intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys)) (intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> u'2'1#(intersect'ii'in(Xs, Ys))) (reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2), intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys)) (reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2), intersect'ii'in#(Xs, cons(X0, Ys)) -> u'1'1#(intersect'ii'in(Xs, Ys))) (reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2), intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys)) (reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2), intersect'ii'in#(cons(X0, Xs), Ys) -> u'2'1#(intersect'ii'in(Xs, Ys))) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF), 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))))) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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)))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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)))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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))))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), 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)))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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)))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), 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))))) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> intersect'ii'in#(F1, F2)) (reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1#(intersect'ii'in(F1, F2))) (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) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF)) (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))) } SCCS: Scc: { reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF)} Scc: {intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys)} SCC: Strict: { reduce'ii'in#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, cons(G2, Gs))), NF), reduce'ii'in#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> reduce'ii'in#(sequent(cons(G1, Fs), Gs), NF), reduce'ii'in#(sequent(Fs, cons(if(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF), reduce'ii'in#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(G1, Gs)), NF), 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), reduce'ii'in#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> reduce'ii'in#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF), reduce'ii'in#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, Fs), Gs), NF), 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), reduce'ii'in#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> reduce'ii'in#(sequent(Fs, cons(F1, Gs)), NF), reduce'ii'in#(sequent(cons(if(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF), reduce'ii'in#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(F1, cons(F2, Fs)), Gs), NF), reduce'ii'in#(sequent(cons(iff(A, B), Fs), Gs), NF) -> reduce'ii'in#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF), reduce'ii'in#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> reduce'ii'in#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right)), reduce'ii'in#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> reduce'ii'in#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right))), u'6'1#(reduce'ii'out(), F2, Fs, Gs, NF) -> reduce'ii'in#(sequent(cons(F2, Fs), Gs), NF), u'12'1#(reduce'ii'out(), Fs, G2, Gs, NF) -> reduce'ii'in#(sequent(Fs, cons(G2, Gs)), NF)} Weak: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)), intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out(), intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)), u'1'1(intersect'ii'out()) -> intersect'ii'out(), u'2'1(intersect'ii'out()) -> intersect'ii'out(), u'3'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)), reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), 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)), 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), 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)), 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), reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), 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)), 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)), 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)), 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))), 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)))), reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2)), u'4'1(reduce'ii'out()) -> reduce'ii'out(), u'5'1(reduce'ii'out()) -> reduce'ii'out(), 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(), 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(), u'10'1(reduce'ii'out()) -> reduce'ii'out(), u'11'1(reduce'ii'out()) -> reduce'ii'out(), 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(), u'13'1(reduce'ii'out()) -> reduce'ii'out(), u'14'1(reduce'ii'out()) -> reduce'ii'out(), u'15'1(intersect'ii'out()) -> reduce'ii'out(), u'16'1(reduce'ii'out()) -> tautology'i'out(), tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))} Fail SCC: Strict: {intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(cons(X0, Xs), Ys) -> intersect'ii'in#(Xs, Ys)} Weak: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)), intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out(), intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)), u'1'1(intersect'ii'out()) -> intersect'ii'out(), u'2'1(intersect'ii'out()) -> intersect'ii'out(), u'3'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)), reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), 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)), 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), 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)), 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), reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), 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)), 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)), 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)), 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))), 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)))), reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2)), u'4'1(reduce'ii'out()) -> reduce'ii'out(), u'5'1(reduce'ii'out()) -> reduce'ii'out(), 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(), 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(), u'10'1(reduce'ii'out()) -> reduce'ii'out(), u'11'1(reduce'ii'out()) -> reduce'ii'out(), 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(), u'13'1(reduce'ii'out()) -> reduce'ii'out(), u'14'1(reduce'ii'out()) -> reduce'ii'out(), u'15'1(intersect'ii'out()) -> reduce'ii'out(), u'16'1(reduce'ii'out()) -> tautology'i'out(), tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))} SPSC: Simple Projection: pi(intersect'ii'in#) = 0 Strict: {intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys)} EDG: {(intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys), intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys))} SCCS: Scc: {intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys)} SCC: Strict: {intersect'ii'in#(Xs, cons(X0, Ys)) -> intersect'ii'in#(Xs, Ys)} Weak: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)), intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out(), intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)), u'1'1(intersect'ii'out()) -> intersect'ii'out(), u'2'1(intersect'ii'out()) -> intersect'ii'out(), u'3'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)), reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), 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)), 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), 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)), 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), reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), 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)), 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)), 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)), 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))), 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)))), reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> u'15'1(intersect'ii'in(F1, F2)), u'4'1(reduce'ii'out()) -> reduce'ii'out(), u'5'1(reduce'ii'out()) -> reduce'ii'out(), 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(), 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(), u'10'1(reduce'ii'out()) -> reduce'ii'out(), u'11'1(reduce'ii'out()) -> reduce'ii'out(), 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(), u'13'1(reduce'ii'out()) -> reduce'ii'out(), u'14'1(reduce'ii'out()) -> reduce'ii'out(), u'15'1(intersect'ii'out()) -> reduce'ii'out(), u'16'1(reduce'ii'out()) -> tautology'i'out(), tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))} SPSC: Simple Projection: pi(intersect'ii'in#) = 1 Strict: {} Qed