%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU028+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n018.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 : Tue Jul 19 14:48:01 EDT 2022 % Result : Theorem 4.18s 4.46s % Output : Proof 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SEU028+1 : TPTP v8.1.0. Released v3.2.0. % 0.00/0.11 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.32 % Computer : n018.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Mon Jun 20 09:25:05 EDT 2022 % 0.11/0.32 % CPUTime : % 4.18/4.46 % SZS status Theorem % 4.18/4.46 (* PROOF-FOUND *) % 4.18/4.46 (* BEGIN-PROOF *) % 4.18/4.46 % SZS output start Proof % 4.18/4.46 1. (relation T_0) (-. (relation T_0)) ### Axiom % 4.18/4.46 2. (function T_0) (-. (function T_0)) ### Axiom % 4.18/4.46 3. (one_to_one T_0) (-. (one_to_one T_0)) ### Axiom % 4.18/4.46 4. (relation T_0) (-. (relation T_0)) ### Axiom % 4.18/4.46 5. (function T_0) (-. (function T_0)) ### Axiom % 4.18/4.46 6. (relation T_0) (-. (relation T_0)) ### Axiom % 4.18/4.46 7. (function T_0) (-. (function T_0)) ### Axiom % 4.18/4.46 8. (-. (relation (function_inverse T_0))) (relation (function_inverse T_0)) ### Axiom % 4.18/4.46 9. ((relation (function_inverse T_0)) /\ (function (function_inverse T_0))) (-. (relation (function_inverse T_0))) ### And 8 % 4.18/4.46 10. (((relation T_0) /\ (function T_0)) => ((relation (function_inverse T_0)) /\ (function (function_inverse T_0)))) (-. (relation (function_inverse T_0))) (function T_0) (relation T_0) ### DisjTree 6 7 9 % 4.18/4.46 11. (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (-. (relation (function_inverse T_0))) ### All 10 % 4.18/4.46 12. (relation T_0) (-. (relation T_0)) ### Axiom % 4.18/4.46 13. (function T_0) (-. (function T_0)) ### Axiom % 4.18/4.46 14. (-. (function (function_inverse T_0))) (function (function_inverse T_0)) ### Axiom % 4.18/4.46 15. ((relation (function_inverse T_0)) /\ (function (function_inverse T_0))) (-. (function (function_inverse T_0))) ### And 14 % 4.18/4.46 16. (((relation T_0) /\ (function T_0)) => ((relation (function_inverse T_0)) /\ (function (function_inverse T_0)))) (-. (function (function_inverse T_0))) (function T_0) (relation T_0) ### DisjTree 12 13 15 % 4.18/4.46 17. (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (-. (function (function_inverse T_0))) ### All 16 % 4.18/4.46 18. (-. (relation (relation_composition T_0 (function_inverse T_0)))) (relation (relation_composition T_0 (function_inverse T_0))) ### Axiom % 4.18/4.46 19. ((relation (relation_composition T_0 (function_inverse T_0))) /\ (function (relation_composition T_0 (function_inverse T_0)))) (-. (relation (relation_composition T_0 (function_inverse T_0)))) ### And 18 % 4.18/4.46 20. (((relation T_0) /\ ((function T_0) /\ ((relation (function_inverse T_0)) /\ (function (function_inverse T_0))))) => ((relation (relation_composition T_0 (function_inverse T_0))) /\ (function (relation_composition T_0 (function_inverse T_0))))) (-. (relation (relation_composition T_0 (function_inverse T_0)))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (function T_0) (relation T_0) ### DisjTree 4 5 11 17 19 % 4.18/4.46 21. (All B, (((relation T_0) /\ ((function T_0) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition T_0 B)) /\ (function (relation_composition T_0 B))))) (relation T_0) (function T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (-. (relation (relation_composition T_0 (function_inverse T_0)))) ### All 20 % 4.18/4.46 22. (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (-. (relation (relation_composition T_0 (function_inverse T_0)))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (function T_0) (relation T_0) ### All 21 % 4.18/4.46 23. (relation T_0) (-. (relation T_0)) ### Axiom % 4.18/4.46 24. (function T_0) (-. (function T_0)) ### Axiom % 4.18/4.46 25. (-. (function (relation_composition T_0 (function_inverse T_0)))) (function (relation_composition T_0 (function_inverse T_0))) ### Axiom % 4.18/4.46 26. ((relation (relation_composition T_0 (function_inverse T_0))) /\ (function (relation_composition T_0 (function_inverse T_0)))) (-. (function (relation_composition T_0 (function_inverse T_0)))) ### And 25 % 4.18/4.46 27. (((relation T_0) /\ ((function T_0) /\ ((relation (function_inverse T_0)) /\ (function (function_inverse T_0))))) => ((relation (relation_composition T_0 (function_inverse T_0))) /\ (function (relation_composition T_0 (function_inverse T_0))))) (-. (function (relation_composition T_0 (function_inverse T_0)))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (function T_0) (relation T_0) ### DisjTree 23 24 11 17 26 % 4.18/4.46 28. (All B, (((relation T_0) /\ ((function T_0) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition T_0 B)) /\ (function (relation_composition T_0 B))))) (relation T_0) (function T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (-. (function (relation_composition T_0 (function_inverse T_0)))) ### All 27 % 4.18/4.46 29. (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (-. (function (relation_composition T_0 (function_inverse T_0)))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (function T_0) (relation T_0) ### All 28 % 4.18/4.46 30. ((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) ((relation_dom (relation_composition T_0 (function_inverse T_0))) != (relation_dom T_0)) ### Axiom % 4.18/4.46 31. (relation T_0) (-. (relation T_0)) ### Axiom % 4.18/4.46 32. (function T_0) (-. (function T_0)) ### Axiom % 4.18/4.46 33. (one_to_one T_0) (-. (one_to_one T_0)) ### Axiom % 4.18/4.46 34. (in T_1 (relation_dom T_0)) (-. (in T_1 (relation_dom T_0))) ### Axiom % 4.18/4.46 35. ((apply (relation_composition T_0 (function_inverse T_0)) T_1) != T_1) (T_1 = (apply (relation_composition T_0 (function_inverse T_0)) T_1)) ### Sym(=) % 4.18/4.46 36. ((T_1 = (apply (function_inverse T_0) (apply T_0 T_1))) /\ (T_1 = (apply (relation_composition T_0 (function_inverse T_0)) T_1))) ((apply (relation_composition T_0 (function_inverse T_0)) T_1) != T_1) ### And 35 % 4.18/4.46 37. (((relation T_0) /\ (function T_0)) => (((one_to_one T_0) /\ (in T_1 (relation_dom T_0))) => ((T_1 = (apply (function_inverse T_0) (apply T_0 T_1))) /\ (T_1 = (apply (relation_composition T_0 (function_inverse T_0)) T_1))))) ((apply (relation_composition T_0 (function_inverse T_0)) T_1) != T_1) (in T_1 (relation_dom T_0)) (one_to_one T_0) (function T_0) (relation T_0) ### DisjTree 31 32 33 34 36 % 4.18/4.46 38. (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in T_1 (relation_dom B))) => ((T_1 = (apply (function_inverse B) (apply B T_1))) /\ (T_1 = (apply (relation_composition B (function_inverse B)) T_1)))))) (relation T_0) (function T_0) (one_to_one T_0) (in T_1 (relation_dom T_0)) ((apply (relation_composition T_0 (function_inverse T_0)) T_1) != T_1) ### All 37 % 4.18/4.46 39. (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) ((apply (relation_composition T_0 (function_inverse T_0)) T_1) != T_1) (in T_1 (relation_dom T_0)) (one_to_one T_0) (function T_0) (relation T_0) ### All 38 % 4.18/4.46 40. (-. ((in T_1 (relation_dom T_0)) => ((apply (relation_composition T_0 (function_inverse T_0)) T_1) = T_1))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) ### NotImply 39 % 4.18/4.46 41. (-. (All C, ((in C (relation_dom T_0)) => ((apply (relation_composition T_0 (function_inverse T_0)) C) = C)))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (one_to_one T_0) (function T_0) (relation T_0) ### NotAllEx 40 % 4.18/4.46 42. (-. (((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply (relation_composition T_0 (function_inverse T_0)) C) = C))))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) ((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) ### NotAnd 30 41 % 4.27/4.49 43. ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) ((relation_composition T_0 (function_inverse T_0)) = (identity_relation (relation_dom T_0))) ### Axiom % 4.27/4.49 44. (((relation_composition T_0 (function_inverse T_0)) = (identity_relation (relation_dom T_0))) <=> (((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply (relation_composition T_0 (function_inverse T_0)) C) = C))))) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) ((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (one_to_one T_0) (function T_0) (relation T_0) ### Equiv 42 43 % 4.27/4.49 45. (((relation (relation_composition T_0 (function_inverse T_0))) /\ (function (relation_composition T_0 (function_inverse T_0)))) => (((relation_composition T_0 (function_inverse T_0)) = (identity_relation (relation_dom T_0))) <=> (((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply (relation_composition T_0 (function_inverse T_0)) C) = C)))))) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) ((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) (relation T_0) (function T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) ### DisjTree 22 29 44 % 4.27/4.49 46. (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_dom T_0))) <=> (((relation_dom B) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply B C) = C))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (function T_0) (relation T_0) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) ((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (one_to_one T_0) ### All 45 % 4.27/4.49 47. (((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) /\ ((relation_rng (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0))) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) (relation T_0) (function T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_dom T_0))) <=> (((relation_dom B) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply B C) = C))))))) ### And 46 % 4.27/4.49 48. (((relation T_0) /\ (function T_0)) => ((one_to_one T_0) => (((relation_dom (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0)) /\ ((relation_rng (relation_composition T_0 (function_inverse T_0))) = (relation_dom T_0))))) (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_dom T_0))) <=> (((relation_dom B) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply B C) = C))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (one_to_one T_0) (function T_0) (relation T_0) ### DisjTree 1 2 3 47 % 4.27/4.49 49. (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition A (function_inverse A))) = (relation_dom A)) /\ ((relation_rng (relation_composition A (function_inverse A))) = (relation_dom A)))))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_dom T_0))) <=> (((relation_dom B) = (relation_dom T_0)) /\ (All C, ((in C (relation_dom T_0)) => ((apply B C) = C))))))) ### All 48 % 4.27/4.49 50. (All A, (All B, (((relation B) /\ (function B)) => ((B = (identity_relation A)) <=> (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = C)))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_composition T_0 (function_inverse T_0)) != (identity_relation (relation_dom T_0))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (one_to_one T_0) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition A (function_inverse A))) = (relation_dom A)) /\ ((relation_rng (relation_composition A (function_inverse A))) = (relation_dom A)))))) ### All 49 % 4.27/4.49 51. (relation T_0) (-. (relation T_0)) ### Axiom % 4.27/4.49 52. (function T_0) (-. (function T_0)) ### Axiom % 4.27/4.49 53. (one_to_one T_0) (-. (one_to_one T_0)) ### Axiom % 4.27/4.49 54. (relation T_0) (-. (relation T_0)) ### Axiom % 4.27/4.49 55. (function T_0) (-. (function T_0)) ### Axiom % 4.27/4.49 56. (-. (relation (relation_composition (function_inverse T_0) T_0))) (relation (relation_composition (function_inverse T_0) T_0)) ### Axiom % 4.27/4.49 57. ((relation (relation_composition (function_inverse T_0) T_0)) /\ (function (relation_composition (function_inverse T_0) T_0))) (-. (relation (relation_composition (function_inverse T_0) T_0))) ### And 56 % 4.33/4.58 58. (((relation (function_inverse T_0)) /\ ((function (function_inverse T_0)) /\ ((relation T_0) /\ (function T_0)))) => ((relation (relation_composition (function_inverse T_0) T_0)) /\ (function (relation_composition (function_inverse T_0) T_0)))) (-. (relation (relation_composition (function_inverse T_0) T_0))) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### DisjTree 11 17 54 55 57 % 4.33/4.58 59. (All B, (((relation (function_inverse T_0)) /\ ((function (function_inverse T_0)) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition (function_inverse T_0) B)) /\ (function (relation_composition (function_inverse T_0) B))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (-. (relation (relation_composition (function_inverse T_0) T_0))) ### All 58 % 4.33/4.58 60. (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (-. (relation (relation_composition (function_inverse T_0) T_0))) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### All 59 % 4.33/4.58 61. (relation T_0) (-. (relation T_0)) ### Axiom % 4.33/4.58 62. (function T_0) (-. (function T_0)) ### Axiom % 4.33/4.58 63. (-. (function (relation_composition (function_inverse T_0) T_0))) (function (relation_composition (function_inverse T_0) T_0)) ### Axiom % 4.33/4.58 64. ((relation (relation_composition (function_inverse T_0) T_0)) /\ (function (relation_composition (function_inverse T_0) T_0))) (-. (function (relation_composition (function_inverse T_0) T_0))) ### And 63 % 4.33/4.58 65. (((relation (function_inverse T_0)) /\ ((function (function_inverse T_0)) /\ ((relation T_0) /\ (function T_0)))) => ((relation (relation_composition (function_inverse T_0) T_0)) /\ (function (relation_composition (function_inverse T_0) T_0)))) (-. (function (relation_composition (function_inverse T_0) T_0))) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### DisjTree 11 17 61 62 64 % 4.33/4.58 66. (All B, (((relation (function_inverse T_0)) /\ ((function (function_inverse T_0)) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition (function_inverse T_0) B)) /\ (function (relation_composition (function_inverse T_0) B))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (-. (function (relation_composition (function_inverse T_0) T_0))) ### All 65 % 4.33/4.58 67. (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (-. (function (relation_composition (function_inverse T_0) T_0))) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### All 66 % 4.33/4.58 68. ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) ### Axiom % 4.33/4.58 69. (relation T_0) (-. (relation T_0)) ### Axiom % 4.33/4.58 70. (function T_0) (-. (function T_0)) ### Axiom % 4.33/4.58 71. (one_to_one T_0) (-. (one_to_one T_0)) ### Axiom % 4.33/4.58 72. (in T_2 (relation_rng T_0)) (-. (in T_2 (relation_rng T_0))) ### Axiom % 4.33/4.58 73. ((apply (relation_composition (function_inverse T_0) T_0) T_2) != T_2) (T_2 = (apply (relation_composition (function_inverse T_0) T_0) T_2)) ### Sym(=) % 4.33/4.58 74. ((T_2 = (apply T_0 (apply (function_inverse T_0) T_2))) /\ (T_2 = (apply (relation_composition (function_inverse T_0) T_0) T_2))) ((apply (relation_composition (function_inverse T_0) T_0) T_2) != T_2) ### And 73 % 4.33/4.58 75. (((relation T_0) /\ (function T_0)) => (((one_to_one T_0) /\ (in T_2 (relation_rng T_0))) => ((T_2 = (apply T_0 (apply (function_inverse T_0) T_2))) /\ (T_2 = (apply (relation_composition (function_inverse T_0) T_0) T_2))))) ((apply (relation_composition (function_inverse T_0) T_0) T_2) != T_2) (in T_2 (relation_rng T_0)) (one_to_one T_0) (function T_0) (relation T_0) ### DisjTree 69 70 71 72 74 % 4.33/4.58 76. (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in T_2 (relation_rng B))) => ((T_2 = (apply B (apply (function_inverse B) T_2))) /\ (T_2 = (apply (relation_composition (function_inverse B) B) T_2)))))) (relation T_0) (function T_0) (one_to_one T_0) (in T_2 (relation_rng T_0)) ((apply (relation_composition (function_inverse T_0) T_0) T_2) != T_2) ### All 75 % 4.33/4.58 77. (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) ((apply (relation_composition (function_inverse T_0) T_0) T_2) != T_2) (in T_2 (relation_rng T_0)) (one_to_one T_0) (function T_0) (relation T_0) ### All 76 % 4.33/4.58 78. (-. ((in T_2 (relation_rng T_0)) => ((apply (relation_composition (function_inverse T_0) T_0) T_2) = T_2))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) ### NotImply 77 % 4.33/4.58 79. (-. (All C, ((in C (relation_rng T_0)) => ((apply (relation_composition (function_inverse T_0) T_0) C) = C)))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (one_to_one T_0) (function T_0) (relation T_0) ### NotAllEx 78 % 4.33/4.58 80. (-. (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply (relation_composition (function_inverse T_0) T_0) C) = C))))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) ### NotAnd 68 79 % 4.33/4.58 81. ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) ((relation_composition (function_inverse T_0) T_0) = (identity_relation (relation_rng T_0))) ### Axiom % 4.33/4.58 82. (((relation_composition (function_inverse T_0) T_0) = (identity_relation (relation_rng T_0))) <=> (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply (relation_composition (function_inverse T_0) T_0) C) = C))))) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (one_to_one T_0) (function T_0) (relation T_0) ### Equiv 80 81 % 4.33/4.58 83. (((relation (relation_composition (function_inverse T_0) T_0)) /\ (function (relation_composition (function_inverse T_0) T_0))) => (((relation_composition (function_inverse T_0) T_0) = (identity_relation (relation_rng T_0))) <=> (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply (relation_composition (function_inverse T_0) T_0) C) = C)))))) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) ### DisjTree 60 67 82 % 4.40/4.62 84. (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_rng T_0))) <=> (((relation_dom B) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply B C) = C))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (one_to_one T_0) ### All 83 % 4.40/4.62 85. (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ ((relation_rng (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0))) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_rng T_0))) <=> (((relation_dom B) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply B C) = C))))))) ### And 84 % 4.40/4.62 86. (((relation T_0) /\ (function T_0)) => ((one_to_one T_0) => (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ ((relation_rng (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0))))) (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_rng T_0))) <=> (((relation_dom B) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply B C) = C))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (one_to_one T_0) (function T_0) (relation T_0) ### DisjTree 51 52 53 85 % 4.40/4.62 87. (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition (function_inverse A) A)) = (relation_rng A)) /\ ((relation_rng (relation_composition (function_inverse A) A)) = (relation_rng A)))))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All B, (((relation B) /\ (function B)) => ((B = (identity_relation (relation_rng T_0))) <=> (((relation_dom B) = (relation_rng T_0)) /\ (All C, ((in C (relation_rng T_0)) => ((apply B C) = C))))))) ### All 86 % 4.40/4.62 88. (All A, (All B, (((relation B) /\ (function B)) => ((B = (identity_relation A)) <=> (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = C)))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_composition (function_inverse T_0) T_0) != (identity_relation (relation_rng T_0))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (one_to_one T_0) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition (function_inverse A) A)) = (relation_rng A)) /\ ((relation_rng (relation_composition (function_inverse A) A)) = (relation_rng A)))))) ### All 87 % 4.40/4.62 89. (-. (((relation_composition T_0 (function_inverse T_0)) = (identity_relation (relation_dom T_0))) /\ ((relation_composition (function_inverse T_0) T_0) = (identity_relation (relation_rng T_0))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition (function_inverse A) A)) = (relation_rng A)) /\ ((relation_rng (relation_composition (function_inverse A) A)) = (relation_rng A)))))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition A (function_inverse A))) = (relation_dom A)) /\ ((relation_rng (relation_composition A (function_inverse A))) = (relation_dom A)))))) (relation T_0) (function T_0) (one_to_one T_0) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (All B, (((relation B) /\ (function B)) => ((B = (identity_relation A)) <=> (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = C)))))))) ### NotAnd 50 88 % 4.40/4.62 90. (-. (((relation T_0) /\ (function T_0)) => ((one_to_one T_0) => (((relation_composition T_0 (function_inverse T_0)) = (identity_relation (relation_dom T_0))) /\ ((relation_composition (function_inverse T_0) T_0) = (identity_relation (relation_rng T_0))))))) (All A, (All B, (((relation B) /\ (function B)) => ((B = (identity_relation A)) <=> (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = C)))))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition A (function_inverse A))) = (relation_dom A)) /\ ((relation_rng (relation_composition A (function_inverse A))) = (relation_dom A)))))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition (function_inverse A) A)) = (relation_rng A)) /\ ((relation_rng (relation_composition (function_inverse A) A)) = (relation_rng A)))))) ### ConjTree 89 % 4.40/4.63 91. (-. (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_composition A (function_inverse A)) = (identity_relation (relation_dom A))) /\ ((relation_composition (function_inverse A) A) = (identity_relation (relation_rng A)))))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition (function_inverse A) A)) = (relation_rng A)) /\ ((relation_rng (relation_composition (function_inverse A) A)) = (relation_rng A)))))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_rng B))) => ((A = (apply B (apply (function_inverse B) A))) /\ (A = (apply (relation_composition (function_inverse B) B) A))))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition A (function_inverse A))) = (relation_dom A)) /\ ((relation_rng (relation_composition A (function_inverse A))) = (relation_dom A)))))) (All A, (All B, (((relation B) /\ (function B)) => (((one_to_one B) /\ (in A (relation_dom B))) => ((A = (apply (function_inverse B) (apply B A))) /\ (A = (apply (relation_composition B (function_inverse B)) A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (All B, (((relation A) /\ ((function A) /\ ((relation B) /\ (function B)))) => ((relation (relation_composition A B)) /\ (function (relation_composition A B)))))) (All A, (All B, (((relation B) /\ (function B)) => ((B = (identity_relation A)) <=> (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = C)))))))) ### NotAllEx 90 % 4.40/4.63 % SZS output end Proof % 4.40/4.63 (* END-PROOF *) %------------------------------------------------------------------------------