%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM013+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Fri Jul 15 01:45:50 EDT 2022 % Result : Theorem 113.88s 114.16s % Output : Proof 114.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : COM013+4 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.15 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.36 % Computer : n023.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Thu Jun 16 17:29:20 EDT 2022 % 0.14/0.37 % CPUTime : % 113.88/114.16 % SZS status Theorem % 113.88/114.16 (* PROOF-FOUND *) % 113.88/114.16 (* BEGIN-PROOF *) % 113.88/114.16 % SZS output start Proof % 113.88/114.16 1. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 113.88/114.16 2. (isTerminating0 (xR)) (-. (isTerminating0 (xR))) ### Axiom % 113.88/114.16 3. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 113.88/114.16 4. (T_0 != T_0) ### Refl(=) % 113.88/114.16 5. (-. ((T_0 = T_0) \/ ((aReductOfIn0 T_0 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_0)))) \/ ((sdtmndtplgtdt0 T_0 (xR) T_0) \/ (sdtmndtasgtdt0 T_0 (xR) T_0)))))) ### ConjTree 4 % 113.88/114.16 6. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 113.88/114.16 7. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 113.88/114.16 8. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 113.88/114.16 9. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 113.88/114.16 10. (aReductOfIn0 T_1 T_0 (xR)) (-. (aReductOfIn0 T_1 T_0 (xR))) ### Axiom % 113.88/114.16 11. (-. (aElement0 T_1)) (aElement0 T_1) ### Axiom % 113.88/114.16 12. ((aReductOfIn0 T_1 T_0 (xR)) => (aElement0 T_1)) (-. (aElement0 T_1)) (aReductOfIn0 T_1 T_0 (xR)) ### Imply 10 11 % 113.88/114.16 13. (All W2, ((aReductOfIn0 W2 T_0 (xR)) => (aElement0 W2))) (aReductOfIn0 T_1 T_0 (xR)) (-. (aElement0 T_1)) ### All 12 % 113.88/114.16 14. (((aElement0 T_0) /\ (aRewritingSystem0 (xR))) => (All W2, ((aReductOfIn0 W2 T_0 (xR)) => (aElement0 W2)))) (-. (aElement0 T_1)) (aReductOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) ### DisjTree 8 9 13 % 113.88/114.16 15. (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (aReductOfIn0 T_1 T_0 (xR)) (-. (aElement0 T_1)) ### All 14 % 113.88/114.16 16. (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (-. (aElement0 T_1)) (aReductOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) ### All 15 % 113.88/114.16 17. (aReductOfIn0 T_1 T_0 (xR)) (-. (aReductOfIn0 T_1 T_0 (xR))) ### Axiom % 113.88/114.16 18. (-. ((aReductOfIn0 T_1 T_0 (xR)) \/ (Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_1)))))) (aReductOfIn0 T_1 T_0 (xR)) ### NotOr 17 % 113.88/114.16 19. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 113.88/114.16 20. (sdtmndtplgtdt0 T_0 (xR) T_1) (-. (sdtmndtplgtdt0 T_0 (xR) T_1)) ### Axiom % 113.88/114.16 21. (-. (iLess0 T_1 T_0)) (iLess0 T_1 T_0) ### Axiom % 113.88/114.16 22. (((aElement0 T_0) /\ (aElement0 T_1)) => ((sdtmndtplgtdt0 T_0 (xR) T_1) => (iLess0 T_1 T_0))) (-. (iLess0 T_1 T_0)) (sdtmndtplgtdt0 T_0 (xR) T_1) (aRewritingSystem0 (xR)) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aElement0 T_0) ### DisjTree 19 16 20 21 % 113.88/114.16 23. (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (aElement0 T_0) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (sdtmndtplgtdt0 T_0 (xR) T_1) (-. (iLess0 T_1 T_0)) ### All 22 % 113.88/114.16 24. (aElement0 T_2) (-. (aElement0 T_2)) ### Axiom % 113.88/114.16 25. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 113.88/114.16 26. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 113.88/114.16 27. (aElement0 T_2) (-. (aElement0 T_2)) ### Axiom % 113.88/114.16 28. (aElement0 T_0) (-. (aElement0 T_0)) ### Axiom % 113.88/114.16 29. (aRewritingSystem0 (xR)) (-. (aRewritingSystem0 (xR))) ### Axiom % 113.88/114.16 30. (sdtmndtplgtdt0 T_0 (xR) T_1) (-. (sdtmndtplgtdt0 T_0 (xR) T_1)) ### Axiom % 113.88/114.16 31. (-. ((T_0 = T_1) \/ (sdtmndtplgtdt0 T_0 (xR) T_1))) (sdtmndtplgtdt0 T_0 (xR) T_1) ### NotOr 30 % 113.88/114.16 32. (-. (sdtmndtasgtdt0 T_0 (xR) T_1)) (sdtmndtasgtdt0 T_0 (xR) T_1) ### Axiom % 113.88/114.16 33. ((sdtmndtasgtdt0 T_0 (xR) T_1) <=> ((T_0 = T_1) \/ (sdtmndtplgtdt0 T_0 (xR) T_1))) (-. (sdtmndtasgtdt0 T_0 (xR) T_1)) (sdtmndtplgtdt0 T_0 (xR) T_1) ### Equiv 31 32 % 113.88/114.16 34. (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 T_1))) => ((sdtmndtasgtdt0 T_0 (xR) T_1) <=> ((T_0 = T_1) \/ (sdtmndtplgtdt0 T_0 (xR) T_1)))) (sdtmndtplgtdt0 T_0 (xR) T_1) (-. (sdtmndtasgtdt0 T_0 (xR) T_1)) (aReductOfIn0 T_1 T_0 (xR)) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aRewritingSystem0 (xR)) (aElement0 T_0) ### DisjTree 28 29 15 33 % 113.88/114.16 35. (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 (xR) W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 (xR) W2))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aReductOfIn0 T_1 T_0 (xR)) (-. (sdtmndtasgtdt0 T_0 (xR) T_1)) (sdtmndtplgtdt0 T_0 (xR) T_1) ### All 34 % 113.88/114.16 36. (sdtmndtasgtdt0 T_1 (xR) T_2) (-. (sdtmndtasgtdt0 T_1 (xR) T_2)) ### Axiom % 113.88/114.16 37. (-. (sdtmndtasgtdt0 T_0 (xR) T_2)) (sdtmndtasgtdt0 T_0 (xR) T_2) ### Axiom % 113.88/114.16 38. (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 T_1) /\ (aElement0 T_2)))) => (((sdtmndtasgtdt0 T_0 (xR) T_1) /\ (sdtmndtasgtdt0 T_1 (xR) T_2)) => (sdtmndtasgtdt0 T_0 (xR) T_2))) (-. (sdtmndtasgtdt0 T_0 (xR) T_2)) (sdtmndtasgtdt0 T_1 (xR) T_2) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 (xR) W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 (xR) W2))))) (aElement0 T_2) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) ### DisjTree 25 26 16 27 35 36 37 % 113.88/114.16 39. (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 T_1) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) T_1) /\ (sdtmndtasgtdt0 T_1 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3)))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (aElement0 T_2) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 (xR) W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 (xR) W2))))) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (sdtmndtasgtdt0 T_1 (xR) T_2) (-. (sdtmndtasgtdt0 T_0 (xR) T_2)) ### All 38 % 113.88/114.16 40. (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (sdtmndtasgtdt0 T_0 (xR) T_2)) (sdtmndtasgtdt0 T_1 (xR) T_2) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aElement0 T_2) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 T_1) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) T_1) /\ (sdtmndtasgtdt0 T_1 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3)))) ### All 39 % 113.88/114.16 41. (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (aElement0 T_2) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (sdtmndtasgtdt0 T_1 (xR) T_2) (-. (sdtmndtasgtdt0 T_0 (xR) T_2)) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) ### All 40 % 113.88/114.16 42. (-. ((T_0 = T_2) \/ ((aReductOfIn0 T_2 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_2)))) \/ ((sdtmndtplgtdt0 T_0 (xR) T_2) \/ (sdtmndtasgtdt0 T_0 (xR) T_2)))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (sdtmndtasgtdt0 T_1 (xR) T_2) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aElement0 T_2) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) ### ConjTree 41 % 114.03/114.24 43. (-. (Ex W3, (aReductOfIn0 W3 T_2 (xR)))) (Ex W3, (aReductOfIn0 W3 T_2 (xR))) ### Axiom % 114.03/114.24 44. (-. ((aElement0 T_2) /\ (((T_0 = T_2) \/ ((aReductOfIn0 T_2 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_2)))) \/ ((sdtmndtplgtdt0 T_0 (xR) T_2) \/ (sdtmndtasgtdt0 T_0 (xR) T_2))))) /\ (-. (Ex W3, (aReductOfIn0 W3 T_2 (xR))))))) (-. (Ex W3, (aReductOfIn0 W3 T_2 (xR)))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (sdtmndtasgtdt0 T_1 (xR) T_2) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_2) ### DisjTree 24 42 43 % 114.03/114.24 45. (-. (((aElement0 T_2) /\ (((T_0 = T_2) \/ ((aReductOfIn0 T_2 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_2)))) \/ ((sdtmndtplgtdt0 T_0 (xR) T_2) \/ (sdtmndtasgtdt0 T_0 (xR) T_2))))) /\ (-. (Ex W3, (aReductOfIn0 W3 T_2 (xR)))))) \/ (aNormalFormOfIn0 T_2 T_0 (xR)))) (aElement0 T_2) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (sdtmndtasgtdt0 T_1 (xR) T_2) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (-. (Ex W3, (aReductOfIn0 W3 T_2 (xR)))) ### NotOr 44 % 114.03/114.24 46. (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (-. (Ex W3, (aReductOfIn0 W3 T_2 (xR)))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (sdtmndtasgtdt0 T_1 (xR) T_2) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_2) ### NotExists 45 % 114.03/114.24 47. ((aElement0 T_2) /\ (((T_1 = T_2) \/ (((aReductOfIn0 T_2 T_1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) T_2))))) /\ (sdtmndtplgtdt0 T_1 (xR) T_2))) /\ ((sdtmndtasgtdt0 T_1 (xR) T_2) /\ ((-. (Ex W3, (aReductOfIn0 W3 T_2 (xR)))) /\ (aNormalFormOfIn0 T_2 T_1 (xR)))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) ### ConjTree 46 % 114.03/114.24 48. (Ex W2, ((aElement0 W2) /\ (((T_1 = W2) \/ (((aReductOfIn0 W2 T_1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 T_1 (xR) W2))) /\ ((sdtmndtasgtdt0 T_1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 T_1 (xR))))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) ### Exists 47 % 114.03/114.24 49. ((aElement0 T_1) => ((iLess0 T_1 T_0) => (Ex W2, ((aElement0 W2) /\ (((T_1 = W2) \/ (((aReductOfIn0 W2 T_1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 T_1 (xR) W2))) /\ ((sdtmndtasgtdt0 T_1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 T_1 (xR))))))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (aReductOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) ### DisjTree 15 23 48 % 114.03/114.30 50. (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W1, (((aElement0 T_0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 T_0 W1) => (aElement0 W2))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (aReductOfIn0 T_1 T_0 (xR)) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) ### All 49 % 114.03/114.30 51. (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (sdtmndtplgtdt0 T_0 (xR) T_1) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (aReductOfIn0 T_1 T_0 (xR)) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) ### All 50 % 114.03/114.30 52. ((sdtmndtplgtdt0 T_0 (xR) T_1) <=> ((aReductOfIn0 T_1 T_0 (xR)) \/ (Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_1)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) ### Equiv 18 51 % 114.03/114.30 53. (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 T_1))) => ((sdtmndtplgtdt0 T_0 (xR) T_1) <=> ((aReductOfIn0 T_1 T_0 (xR)) \/ (Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_1))))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) ### DisjTree 6 7 16 52 % 114.03/114.30 54. (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 (xR) W2) /\ (sdtmndtasgtdt0 W2 (xR) W3)) => (sdtmndtasgtdt0 T_0 (xR) W3))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) ### All 53 % 114.03/114.30 55. (All W1, (All W2, (All W3, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 T_0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 T_0 W1 W3)))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (aReductOfIn0 T_1 T_0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) ### All 54 % 114.34/114.60 56. (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (aElement0 T_0) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aReductOfIn0 T_1 T_0 (xR)) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) ### All 55 % 114.34/114.60 57. (Ex W3, (aReductOfIn0 W3 T_0 (xR))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (aElement0 T_0) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ### Exists 56 % 114.34/114.60 58. (-. ((aElement0 T_0) /\ (((T_0 = T_0) \/ ((aReductOfIn0 T_0 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_0)))) \/ ((sdtmndtplgtdt0 T_0 (xR) T_0) \/ (sdtmndtasgtdt0 T_0 (xR) T_0))))) /\ (-. (Ex W3, (aReductOfIn0 W3 T_0 (xR))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_0) ### DisjTree 3 5 57 % 114.34/114.60 59. (-. (((aElement0 T_0) /\ (((T_0 = T_0) \/ ((aReductOfIn0 T_0 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) T_0)))) \/ ((sdtmndtplgtdt0 T_0 (xR) T_0) \/ (sdtmndtasgtdt0 T_0 (xR) T_0))))) /\ (-. (Ex W3, (aReductOfIn0 W3 T_0 (xR)))))) \/ (aNormalFormOfIn0 T_0 T_0 (xR)))) (aElement0 T_0) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ### NotOr 58 % 114.41/114.63 60. (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W2, (((aElement0 T_0) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 T_0 (xR) W2) => (iLess0 W2 T_0)))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_0) ### NotExists 59 % 114.41/114.63 61. (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 (xR) W2) => (iLess0 W2 W1))))) (aElement0 T_0) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (aRewritingSystem0 (xR)) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) ### All 60 % 114.41/114.63 62. ((isTerminating0 (xR)) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 (xR) W2) => (iLess0 W2 W1)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_0) (isTerminating0 (xR)) ### Equiv 2 61 % 114.41/114.63 63. ((aRewritingSystem0 (xR)) => ((isTerminating0 (xR)) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 (xR) W2) => (iLess0 W2 W1))))))) (isTerminating0 (xR)) (aElement0 T_0) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (aRewritingSystem0 (xR)) ### Imply 1 62 % 114.41/114.63 64. (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 (xR)) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 (xR) W2) <=> ((aReductOfIn0 W2 T_0 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2)))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_0) (isTerminating0 (xR)) ### All 63 % 114.41/114.64 65. (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 T_0 W1 W2) <=> ((aReductOfIn0 W2 T_0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 T_0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2))))))))) (isTerminating0 (xR)) (aElement0 T_0) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (aRewritingSystem0 (xR)) (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) ### All 64 % 114.41/114.64 66. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) (aRewritingSystem0 (xR)) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, (All W2, (((aElement0 T_0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 T_0 W1 W2) <=> ((T_0 = W2) \/ (sdtmndtplgtdt0 T_0 W1 W2)))))) (aElement0 T_0) (isTerminating0 (xR)) ### All 65 % 114.41/114.64 67. (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (isTerminating0 (xR)) (aElement0 T_0) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (aRewritingSystem0 (xR)) (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) ### All 66 % 114.41/114.64 68. ((aRewritingSystem0 (xR)) /\ ((All W0, (All W1, (((aElement0 W0) /\ (aElement0 W1)) => (((aReductOfIn0 W1 W0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 W0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ (sdtmndtplgtdt0 W0 (xR) W1))) => (iLess0 W1 W0))))) /\ (isTerminating0 (xR)))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) (-. (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))) (aElement0 T_0) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) ### ConjTree 67 % 114.41/114.64 69. (-. ((aElement0 T_0) => ((All W1, ((aElement0 W1) => ((iLess0 W1 T_0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) => (Ex W1, (((aElement0 W1) /\ (((T_0 = W1) \/ ((aReductOfIn0 W1 T_0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 T_0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 T_0 (xR) W1) \/ (sdtmndtasgtdt0 T_0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 T_0 (xR))))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) ((aRewritingSystem0 (xR)) /\ ((All W0, (All W1, (((aElement0 W0) /\ (aElement0 W1)) => (((aReductOfIn0 W1 W0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 W0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ (sdtmndtplgtdt0 W0 (xR) W1))) => (iLess0 W1 W0))))) /\ (isTerminating0 (xR)))) ### ConjTree 68 % 114.41/114.64 70. (-. (All W0, ((aElement0 W0) => ((All W1, ((aElement0 W1) => ((iLess0 W1 W0) => (Ex W2, ((aElement0 W2) /\ (((W1 = W2) \/ (((aReductOfIn0 W2 W1 (xR)) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W1 (xR)) /\ (sdtmndtplgtdt0 W3 (xR) W2))))) /\ (sdtmndtplgtdt0 W1 (xR) W2))) /\ ((sdtmndtasgtdt0 W1 (xR) W2) /\ ((-. (Ex W3, (aReductOfIn0 W3 W2 (xR)))) /\ (aNormalFormOfIn0 W2 W1 (xR)))))))))) => (Ex W1, (((aElement0 W1) /\ (((W0 = W1) \/ ((aReductOfIn0 W1 W0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 W0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ ((sdtmndtplgtdt0 W0 (xR) W1) \/ (sdtmndtasgtdt0 W0 (xR) W1))))) /\ (-. (Ex W2, (aReductOfIn0 W2 W1 (xR)))))) \/ (aNormalFormOfIn0 W1 W0 (xR)))))))) ((aRewritingSystem0 (xR)) /\ ((All W0, (All W1, (((aElement0 W0) /\ (aElement0 W1)) => (((aReductOfIn0 W1 W0 (xR)) \/ ((Ex W2, ((aElement0 W2) /\ ((aReductOfIn0 W2 W0 (xR)) /\ (sdtmndtplgtdt0 W2 (xR) W1)))) \/ (sdtmndtplgtdt0 W0 (xR) W1))) => (iLess0 W1 W0))))) /\ (isTerminating0 (xR)))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtplgtdt0 W0 W1 W2) <=> ((aReductOfIn0 W2 W0 W1) \/ (Ex W3, ((aElement0 W3) /\ ((aReductOfIn0 W3 W0 W1) /\ (sdtmndtplgtdt0 W3 W1 W2)))))))))) (All W0, ((aRewritingSystem0 W0) => ((isTerminating0 W0) <=> (All W1, (All W2, (((aElement0 W1) /\ (aElement0 W2)) => ((sdtmndtplgtdt0 W1 W0 W2) => (iLess0 W2 W1)))))))) (All W0, (All W1, (All W2, (All W3, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ ((aElement0 W2) /\ (aElement0 W3)))) => (((sdtmndtasgtdt0 W0 W1 W2) /\ (sdtmndtasgtdt0 W2 W1 W3)) => (sdtmndtasgtdt0 W0 W1 W3))))))) (All W0, (All W1, (((aElement0 W0) /\ (aRewritingSystem0 W1)) => (All W2, ((aReductOfIn0 W2 W0 W1) => (aElement0 W2)))))) (All W0, (All W1, (All W2, (((aElement0 W0) /\ ((aRewritingSystem0 W1) /\ (aElement0 W2))) => ((sdtmndtasgtdt0 W0 W1 W2) <=> ((W0 = W2) \/ (sdtmndtplgtdt0 W0 W1 W2))))))) ### NotAllEx 69 % 114.41/114.64 % SZS output end Proof % 114.41/114.64 (* END-PROOF *) %------------------------------------------------------------------------------