%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : ALG189+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n025.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 : Thu Jul 14 18:31:04 EDT 2022 % Result : Theorem 1.08s 1.30s % Output : Proof 1.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG189+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 9 01:27:05 EDT 2022 % 0.13/0.33 % CPUTime : % 1.08/1.30 (* PROOF-FOUND *) % 1.08/1.30 % SZS status Theorem % 1.08/1.30 (* BEGIN-PROOF *) % 1.08/1.30 % SZS output start Proof % 1.08/1.30 Theorem co1 : (((op (op (e0) (e0)) (e0)) = (e0))/\(((op (op (e0) (e1)) (e1)) = (e0))/\(((op (op (e0) (e2)) (e2)) = (e0))/\(((op (op (e0) (e3)) (e3)) = (e0))/\(((op (op (e0) (e4)) (e4)) = (e0))/\(((op (op (e1) (e0)) (e0)) = (e1))/\(((op (op (e1) (e1)) (e1)) = (e1))/\(((op (op (e1) (e2)) (e2)) = (e1))/\(((op (op (e1) (e3)) (e3)) = (e1))/\(((op (op (e1) (e4)) (e4)) = (e1))/\(((op (op (e2) (e0)) (e0)) = (e2))/\(((op (op (e2) (e1)) (e1)) = (e2))/\(((op (op (e2) (e2)) (e2)) = (e2))/\(((op (op (e2) (e3)) (e3)) = (e2))/\(((op (op (e2) (e4)) (e4)) = (e2))/\(((op (op (e3) (e0)) (e0)) = (e3))/\(((op (op (e3) (e1)) (e1)) = (e3))/\(((op (op (e3) (e2)) (e2)) = (e3))/\(((op (op (e3) (e3)) (e3)) = (e3))/\(((op (op (e3) (e4)) (e4)) = (e3))/\(((op (op (e4) (e0)) (e0)) = (e4))/\(((op (op (e4) (e1)) (e1)) = (e4))/\(((op (op (e4) (e2)) (e2)) = (e4))/\(((op (op (e4) (e3)) (e3)) = (e4))/\(((op (op (e4) (e4)) (e4)) = (e4))/\((((op (e0) (e0)) = (e0))\/(((op (e0) (e0)) = (e1))\/(((op (e0) (e0)) = (e2))\/(((op (e0) (e0)) = (e3))\/((op (e0) (e0)) = (e4))))))/\((((op (e0) (e1)) = (e0))\/(((op (e0) (e1)) = (e1))\/(((op (e0) (e1)) = (e2))\/(((op (e0) (e1)) = (e3))\/((op (e0) (e1)) = (e4))))))/\((((op (e0) (e2)) = (e0))\/(((op (e0) (e2)) = (e1))\/(((op (e0) (e2)) = (e2))\/(((op (e0) (e2)) = (e3))\/((op (e0) (e2)) = (e4))))))/\((((op (e0) (e3)) = (e0))\/(((op (e0) (e3)) = (e1))\/(((op (e0) (e3)) = (e2))\/(((op (e0) (e3)) = (e3))\/((op (e0) (e3)) = (e4))))))/\((((op (e0) (e4)) = (e0))\/(((op (e0) (e4)) = (e1))\/(((op (e0) (e4)) = (e2))\/(((op (e0) (e4)) = (e3))\/((op (e0) (e4)) = (e4))))))/\((((op (e1) (e0)) = (e0))\/(((op (e1) (e0)) = (e1))\/(((op (e1) (e0)) = (e2))\/(((op (e1) (e0)) = (e3))\/((op (e1) (e0)) = (e4))))))/\((((op (e1) (e1)) = (e0))\/(((op (e1) (e1)) = (e1))\/(((op (e1) (e1)) = (e2))\/(((op (e1) (e1)) = (e3))\/((op (e1) (e1)) = (e4))))))/\((((op (e1) (e2)) = (e0))\/(((op (e1) (e2)) = (e1))\/(((op (e1) (e2)) = (e2))\/(((op (e1) (e2)) = (e3))\/((op (e1) (e2)) = (e4))))))/\((((op (e1) (e3)) = (e0))\/(((op (e1) (e3)) = (e1))\/(((op (e1) (e3)) = (e2))\/(((op (e1) (e3)) = (e3))\/((op (e1) (e3)) = (e4))))))/\((((op (e1) (e4)) = (e0))\/(((op (e1) (e4)) = (e1))\/(((op (e1) (e4)) = (e2))\/(((op (e1) (e4)) = (e3))\/((op (e1) (e4)) = (e4))))))/\((((op (e2) (e0)) = (e0))\/(((op (e2) (e0)) = (e1))\/(((op (e2) (e0)) = (e2))\/(((op (e2) (e0)) = (e3))\/((op (e2) (e0)) = (e4))))))/\((((op (e2) (e1)) = (e0))\/(((op (e2) (e1)) = (e1))\/(((op (e2) (e1)) = (e2))\/(((op (e2) (e1)) = (e3))\/((op (e2) (e1)) = (e4))))))/\((((op (e2) (e2)) = (e0))\/(((op (e2) (e2)) = (e1))\/(((op (e2) (e2)) = (e2))\/(((op (e2) (e2)) = (e3))\/((op (e2) (e2)) = (e4))))))/\((((op (e2) (e3)) = (e0))\/(((op (e2) (e3)) = (e1))\/(((op (e2) (e3)) = (e2))\/(((op (e2) (e3)) = (e3))\/((op (e2) (e3)) = (e4))))))/\((((op (e2) (e4)) = (e0))\/(((op (e2) (e4)) = (e1))\/(((op (e2) (e4)) = (e2))\/(((op (e2) (e4)) = (e3))\/((op (e2) (e4)) = (e4))))))/\((((op (e3) (e0)) = (e0))\/(((op (e3) (e0)) = (e1))\/(((op (e3) (e0)) = (e2))\/(((op (e3) (e0)) = (e3))\/((op (e3) (e0)) = (e4))))))/\((((op (e3) (e1)) = (e0))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e1)) = (e2))\/(((op (e3) (e1)) = (e3))\/((op (e3) (e1)) = (e4))))))/\((((op (e3) (e2)) = (e0))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e2)) = (e2))\/(((op (e3) (e2)) = (e3))\/((op (e3) (e2)) = (e4))))))/\((((op (e3) (e3)) = (e0))\/(((op (e3) (e3)) = (e1))\/(((op (e3) (e3)) = (e2))\/(((op (e3) (e3)) = (e3))\/((op (e3) (e3)) = (e4))))))/\((((op (e3) (e4)) = (e0))\/(((op (e3) (e4)) = (e1))\/(((op (e3) (e4)) = (e2))\/(((op (e3) (e4)) = (e3))\/((op (e3) (e4)) = (e4))))))/\((((op (e4) (e0)) = (e0))\/(((op (e4) (e0)) = (e1))\/(((op (e4) (e0)) = (e2))\/(((op (e4) (e0)) = (e3))\/((op (e4) (e0)) = (e4))))))/\((((op (e4) (e1)) = (e0))\/(((op (e4) (e1)) = (e1))\/(((op (e4) (e1)) = (e2))\/(((op (e4) (e1)) = (e3))\/((op (e4) (e1)) = (e4))))))/\((((op (e4) (e2)) = (e0))\/(((op (e4) (e2)) = (e1))\/(((op (e4) (e2)) = (e2))\/(((op (e4) (e2)) = (e3))\/((op (e4) (e2)) = (e4))))))/\((((op (e4) (e3)) = (e0))\/(((op (e4) (e3)) = (e1))\/(((op (e4) (e3)) = (e2))\/(((op (e4) (e3)) = (e3))\/((op (e4) (e3)) = (e4))))))/\((((op (e4) (e4)) = (e0))\/(((op (e4) (e4)) = (e1))\/(((op (e4) (e4)) = (e2))\/(((op (e4) (e4)) = (e3))\/((op (e4) (e4)) = (e4))))))/\((((op (e0) (e0)) = (e0))\/(((op (e0) (e1)) = (e0))\/(((op (e0) (e2)) = (e0))\/(((op (e0) (e3)) = (e0))\/((op (e0) (e4)) = (e0))))))/\((((op (e0) (e0)) = (e0))\/(((op (e1) (e0)) = (e0))\/(((op (e2) (e0)) = (e0))\/(((op (e3) (e0)) = (e0))\/((op (e4) (e0)) = (e0))))))/\((((op (e0) (e0)) = (e1))\/(((op (e0) (e1)) = (e1))\/(((op (e0) (e2)) = (e1))\/(((op (e0) (e3)) = (e1))\/((op (e0) (e4)) = (e1))))))/\((((op (e0) (e0)) = (e1))\/(((op (e1) (e0)) = (e1))\/(((op (e2) (e0)) = (e1))\/(((op (e3) (e0)) = (e1))\/((op (e4) (e0)) = (e1))))))/\((((op (e0) (e0)) = (e2))\/(((op (e0) (e1)) = (e2))\/(((op (e0) (e2)) = (e2))\/(((op (e0) (e3)) = (e2))\/((op (e0) (e4)) = (e2))))))/\((((op (e0) (e0)) = (e2))\/(((op (e1) (e0)) = (e2))\/(((op (e2) (e0)) = (e2))\/(((op (e3) (e0)) = (e2))\/((op (e4) (e0)) = (e2))))))/\((((op (e0) (e0)) = (e3))\/(((op (e0) (e1)) = (e3))\/(((op (e0) (e2)) = (e3))\/(((op (e0) (e3)) = (e3))\/((op (e0) (e4)) = (e3))))))/\((((op (e0) (e0)) = (e3))\/(((op (e1) (e0)) = (e3))\/(((op (e2) (e0)) = (e3))\/(((op (e3) (e0)) = (e3))\/((op (e4) (e0)) = (e3))))))/\((((op (e0) (e0)) = (e4))\/(((op (e0) (e1)) = (e4))\/(((op (e0) (e2)) = (e4))\/(((op (e0) (e3)) = (e4))\/((op (e0) (e4)) = (e4))))))/\((((op (e0) (e0)) = (e4))\/(((op (e1) (e0)) = (e4))\/(((op (e2) (e0)) = (e4))\/(((op (e3) (e0)) = (e4))\/((op (e4) (e0)) = (e4))))))/\((((op (e1) (e0)) = (e0))\/(((op (e1) (e1)) = (e0))\/(((op (e1) (e2)) = (e0))\/(((op (e1) (e3)) = (e0))\/((op (e1) (e4)) = (e0))))))/\((((op (e0) (e1)) = (e0))\/(((op (e1) (e1)) = (e0))\/(((op (e2) (e1)) = (e0))\/(((op (e3) (e1)) = (e0))\/((op (e4) (e1)) = (e0))))))/\((((op (e1) (e0)) = (e1))\/(((op (e1) (e1)) = (e1))\/(((op (e1) (e2)) = (e1))\/(((op (e1) (e3)) = (e1))\/((op (e1) (e4)) = (e1))))))/\((((op (e0) (e1)) = (e1))\/(((op (e1) (e1)) = (e1))\/(((op (e2) (e1)) = (e1))\/(((op (e3) (e1)) = (e1))\/((op (e4) (e1)) = (e1))))))/\((((op (e1) (e0)) = (e2))\/(((op (e1) (e1)) = (e2))\/(((op (e1) (e2)) = (e2))\/(((op (e1) (e3)) = (e2))\/((op (e1) (e4)) = (e2))))))/\((((op (e0) (e1)) = (e2))\/(((op (e1) (e1)) = (e2))\/(((op (e2) (e1)) = (e2))\/(((op (e3) (e1)) = (e2))\/((op (e4) (e1)) = (e2))))))/\((((op (e1) (e0)) = (e3))\/(((op (e1) (e1)) = (e3))\/(((op (e1) (e2)) = (e3))\/(((op (e1) (e3)) = (e3))\/((op (e1) (e4)) = (e3))))))/\((((op (e0) (e1)) = (e3))\/(((op (e1) (e1)) = (e3))\/(((op (e2) (e1)) = (e3))\/(((op (e3) (e1)) = (e3))\/((op (e4) (e1)) = (e3))))))/\((((op (e1) (e0)) = (e4))\/(((op (e1) (e1)) = (e4))\/(((op (e1) (e2)) = (e4))\/(((op (e1) (e3)) = (e4))\/((op (e1) (e4)) = (e4))))))/\((((op (e0) (e1)) = (e4))\/(((op (e1) (e1)) = (e4))\/(((op (e2) (e1)) = (e4))\/(((op (e3) (e1)) = (e4))\/((op (e4) (e1)) = (e4))))))/\((((op (e2) (e0)) = (e0))\/(((op (e2) (e1)) = (e0))\/(((op (e2) (e2)) = (e0))\/(((op (e2) (e3)) = (e0))\/((op (e2) (e4)) = (e0))))))/\((((op (e0) (e2)) = (e0))\/(((op (e1) (e2)) = (e0))\/(((op (e2) (e2)) = (e0))\/(((op (e3) (e2)) = (e0))\/((op (e4) (e2)) = (e0))))))/\((((op (e2) (e0)) = (e1))\/(((op (e2) (e1)) = (e1))\/(((op (e2) (e2)) = (e1))\/(((op (e2) (e3)) = (e1))\/((op (e2) (e4)) = (e1))))))/\((((op (e0) (e2)) = (e1))\/(((op (e1) (e2)) = (e1))\/(((op (e2) (e2)) = (e1))\/(((op (e3) (e2)) = (e1))\/((op (e4) (e2)) = (e1))))))/\((((op (e2) (e0)) = (e2))\/(((op (e2) (e1)) = (e2))\/(((op (e2) (e2)) = (e2))\/(((op (e2) (e3)) = (e2))\/((op (e2) (e4)) = (e2))))))/\((((op (e0) (e2)) = (e2))\/(((op (e1) (e2)) = (e2))\/(((op (e2) (e2)) = (e2))\/(((op (e3) (e2)) = (e2))\/((op (e4) (e2)) = (e2))))))/\((((op (e2) (e0)) = (e3))\/(((op (e2) (e1)) = (e3))\/(((op (e2) (e2)) = (e3))\/(((op (e2) (e3)) = (e3))\/((op (e2) (e4)) = (e3))))))/\((((op (e0) (e2)) = (e3))\/(((op (e1) (e2)) = (e3))\/(((op (e2) (e2)) = (e3))\/(((op (e3) (e2)) = (e3))\/((op (e4) (e2)) = (e3))))))/\((((op (e2) (e0)) = (e4))\/(((op (e2) (e1)) = (e4))\/(((op (e2) (e2)) = (e4))\/(((op (e2) (e3)) = (e4))\/((op (e2) (e4)) = (e4))))))/\((((op (e0) (e2)) = (e4))\/(((op (e1) (e2)) = (e4))\/(((op (e2) (e2)) = (e4))\/(((op (e3) (e2)) = (e4))\/((op (e4) (e2)) = (e4))))))/\((((op (e3) (e0)) = (e0))\/(((op (e3) (e1)) = (e0))\/(((op (e3) (e2)) = (e0))\/(((op (e3) (e3)) = (e0))\/((op (e3) (e4)) = (e0))))))/\((((op (e0) (e3)) = (e0))\/(((op (e1) (e3)) = (e0))\/(((op (e2) (e3)) = (e0))\/(((op (e3) (e3)) = (e0))\/((op (e4) (e3)) = (e0))))))/\((((op (e3) (e0)) = (e1))\/(((op (e3) (e1)) = (e1))\/(((op (e3) (e2)) = (e1))\/(((op (e3) (e3)) = (e1))\/((op (e3) (e4)) = (e1))))))/\((((op (e0) (e3)) = (e1))\/(((op (e1) (e3)) = (e1))\/(((op (e2) (e3)) = (e1))\/(((op (e3) (e3)) = (e1))\/((op (e4) (e3)) = (e1))))))/\((((op (e3) (e0)) = (e2))\/(((op (e3) (e1)) = (e2))\/(((op (e3) (e2)) = (e2))\/(((op (e3) (e3)) = (e2))\/((op (e3) (e4)) = (e2))))))/\((((op (e0) (e3)) = (e2))\/(((op (e1) (e3)) = (e2))\/(((op (e2) (e3)) = (e2))\/(((op (e3) (e3)) = (e2))\/((op (e4) (e3)) = (e2))))))/\((((op (e3) (e0)) = (e3))\/(((op (e3) (e1)) = (e3))\/(((op (e3) (e2)) = (e3))\/(((op (e3) (e3)) = (e3))\/((op (e3) (e4)) = (e3))))))/\((((op (e0) (e3)) = (e3))\/(((op (e1) (e3)) = (e3))\/(((op (e2) (e3)) = (e3))\/(((op (e3) (e3)) = (e3))\/((op (e4) (e3)) = (e3))))))/\((((op (e3) (e0)) = (e4))\/(((op (e3) (e1)) = (e4))\/(((op (e3) (e2)) = (e4))\/(((op (e3) (e3)) = (e4))\/((op (e3) (e4)) = (e4))))))/\((((op (e0) (e3)) = (e4))\/(((op (e1) (e3)) = (e4))\/(((op (e2) (e3)) = (e4))\/(((op (e3) (e3)) = (e4))\/((op (e4) (e3)) = (e4))))))/\((((op (e4) (e0)) = (e0))\/(((op (e4) (e1)) = (e0))\/(((op (e4) (e2)) = (e0))\/(((op (e4) (e3)) = (e0))\/((op (e4) (e4)) = (e0))))))/\((((op (e0) (e4)) = (e0))\/(((op (e1) (e4)) = (e0))\/(((op (e2) (e4)) = (e0))\/(((op (e3) (e4)) = (e0))\/((op (e4) (e4)) = (e0))))))/\((((op (e4) (e0)) = (e1))\/(((op (e4) (e1)) = (e1))\/(((op (e4) (e2)) = (e1))\/(((op (e4) (e3)) = (e1))\/((op (e4) (e4)) = (e1))))))/\((((op (e0) (e4)) = (e1))\/(((op (e1) (e4)) = (e1))\/(((op (e2) (e4)) = (e1))\/(((op (e3) (e4)) = (e1))\/((op (e4) (e4)) = (e1))))))/\((((op (e4) (e0)) = (e2))\/(((op (e4) (e1)) = (e2))\/(((op (e4) (e2)) = (e2))\/(((op (e4) (e3)) = (e2))\/((op (e4) (e4)) = (e2))))))/\((((op (e0) (e4)) = (e2))\/(((op (e1) (e4)) = (e2))\/(((op (e2) (e4)) = (e2))\/(((op (e3) (e4)) = (e2))\/((op (e4) (e4)) = (e2))))))/\((((op (e4) (e0)) = (e3))\/(((op (e4) (e1)) = (e3))\/(((op (e4) (e2)) = (e3))\/(((op (e4) (e3)) = (e3))\/((op (e4) (e4)) = (e3))))))/\((((op (e0) (e4)) = (e3))\/(((op (e1) (e4)) = (e3))\/(((op (e2) (e4)) = (e3))\/(((op (e3) (e4)) = (e3))\/((op (e4) (e4)) = (e3))))))/\((((op (e4) (e0)) = (e4))\/(((op (e4) (e1)) = (e4))\/(((op (e4) (e2)) = (e4))\/(((op (e4) (e3)) = (e4))\/((op (e4) (e4)) = (e4))))))/\((((op (e0) (e4)) = (e4))\/(((op (e1) (e4)) = (e4))\/(((op (e2) (e4)) = (e4))\/(((op (e3) (e4)) = (e4))\/((op (e4) (e4)) = (e4))))))/\(((op (op (e0) (e0)) (op (e0) (e0))) = (e0))/\(((op (op (e1) (e0)) (op (e0) (e1))) = (e0))/\(((op (op (e2) (e0)) (op (e0) (e2))) = (e0))/\(((op (op (e3) (e0)) (op (e0) (e3))) = (e0))/\(((op (op (e4) (e0)) (op (e0) (e4))) = (e0))/\(((op (op (e0) (e1)) (op (e1) (e0))) = (e1))/\(((op (op (e1) (e1)) (op (e1) (e1))) = (e1))/\(((op (op (e2) (e1)) (op (e1) (e2))) = (e1))/\(((op (op (e3) (e1)) (op (e1) (e3))) = (e1))/\(((op (op (e4) (e1)) (op (e1) (e4))) = (e1))/\(((op (op (e0) (e2)) (op (e2) (e0))) = (e2))/\(((op (op (e1) (e2)) (op (e2) (e1))) = (e2))/\(((op (op (e2) (e2)) (op (e2) (e2))) = (e2))/\(((op (op (e3) (e2)) (op (e2) (e3))) = (e2))/\(((op (op (e4) (e2)) (op (e2) (e4))) = (e2))/\(((op (op (e0) (e3)) (op (e3) (e0))) = (e3))/\(((op (op (e1) (e3)) (op (e3) (e1))) = (e3))/\(((op (op (e2) (e3)) (op (e3) (e2))) = (e3))/\(((op (op (e3) (e3)) (op (e3) (e3))) = (e3))/\(((op (op (e4) (e3)) (op (e3) (e4))) = (e3))/\(((op (op (e0) (e4)) (op (e4) (e0))) = (e4))/\(((op (op (e1) (e4)) (op (e4) (e1))) = (e4))/\(((op (op (e2) (e4)) (op (e4) (e2))) = (e4))/\(((op (op (e3) (e4)) (op (e4) (e3))) = (e4))/\((op (op (e4) (e4)) (op (e4) (e4))) = (e4)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 1.08/1.30 Proof. % 1.08/1.30 assert (zenon_L1_ : (~((e0) = (e0))) -> False). % 1.08/1.30 do 0 intro. intros zenon_H3. % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 (* end of lemma zenon_L1_ *) % 1.08/1.30 assert (zenon_L2_ : (~((e1) = (e1))) -> False). % 1.08/1.30 do 0 intro. intros zenon_H4. % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 (* end of lemma zenon_L2_ *) % 1.08/1.30 assert (zenon_L3_ : (~((e2) = (e2))) -> False). % 1.08/1.30 do 0 intro. intros zenon_H5. % 1.08/1.30 apply zenon_H5. apply refl_equal. % 1.08/1.30 (* end of lemma zenon_L3_ *) % 1.08/1.30 assert (zenon_L4_ : (~((e3) = (e3))) -> False). % 1.08/1.30 do 0 intro. intros zenon_H6. % 1.08/1.30 apply zenon_H6. apply refl_equal. % 1.08/1.30 (* end of lemma zenon_L4_ *) % 1.08/1.30 assert (zenon_L5_ : (~((e4) = (e4))) -> False). % 1.08/1.30 do 0 intro. intros zenon_H7. % 1.08/1.30 apply zenon_H7. apply refl_equal. % 1.08/1.30 (* end of lemma zenon_L5_ *) % 1.08/1.30 apply NNPP. intro zenon_G. % 1.08/1.30 apply (zenon_and_s _ _ ax2). zenon_intro zenon_H9. zenon_intro zenon_H8. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H8). zenon_intro zenon_Hb. zenon_intro zenon_Ha. % 1.08/1.30 apply (zenon_and_s _ _ zenon_Ha). zenon_intro zenon_Hd. zenon_intro zenon_Hc. % 1.08/1.30 apply (zenon_and_s _ _ zenon_Hc). zenon_intro zenon_Hf. zenon_intro zenon_He. % 1.08/1.30 apply (zenon_and_s _ _ zenon_He). zenon_intro zenon_H11. zenon_intro zenon_H10. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H10). zenon_intro zenon_H13. zenon_intro zenon_H12. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H12). zenon_intro zenon_H15. zenon_intro zenon_H14. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H14). zenon_intro zenon_H17. zenon_intro zenon_H16. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H16). zenon_intro zenon_H19. zenon_intro zenon_H18. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H18). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H1a). zenon_intro zenon_H1d. zenon_intro zenon_H1c. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H1c). zenon_intro zenon_H1f. zenon_intro zenon_H1e. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H1e). zenon_intro zenon_H21. zenon_intro zenon_H20. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H20). zenon_intro zenon_H23. zenon_intro zenon_H22. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H22). zenon_intro zenon_H25. zenon_intro zenon_H24. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H24). zenon_intro zenon_H27. zenon_intro zenon_H26. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H26). zenon_intro zenon_H29. zenon_intro zenon_H28. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H28). zenon_intro zenon_H2b. zenon_intro zenon_H2a. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H2a). zenon_intro zenon_H2d. zenon_intro zenon_H2c. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H2c). zenon_intro zenon_H2f. zenon_intro zenon_H2e. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H2e). zenon_intro zenon_H31. zenon_intro zenon_H30. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H30). zenon_intro zenon_H33. zenon_intro zenon_H32. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H32). zenon_intro zenon_H35. zenon_intro zenon_H34. % 1.08/1.30 apply (zenon_and_s _ _ zenon_H34). zenon_intro zenon_H37. zenon_intro zenon_H36. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_G); [ zenon_intro zenon_H39 | zenon_intro zenon_H38 ]. % 1.08/1.30 cut (((op (e0) (e0)) = (e0)) = ((op (op (e0) (e0)) (e0)) = (e0))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H39. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H9. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e0) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H3a]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [ zenon_intro zenon_H3b | zenon_intro zenon_H3c ]. % 1.08/1.30 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0))) = ((op (e0) (e0)) = (op (op (e0) (e0)) (e0)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H3a. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H3b. % 1.08/1.30 cut (((op (op (e0) (e0)) (e0)) = (op (op (e0) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H3c]. % 1.08/1.30 cut (((op (op (e0) (e0)) (e0)) = (op (e0) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H3d]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e0) (e0)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H3e zenon_H9). % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply zenon_H3c. apply refl_equal. % 1.08/1.30 apply zenon_H3c. apply refl_equal. % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H38); [ zenon_intro zenon_H40 | zenon_intro zenon_H3f ]. % 1.08/1.30 cut (((op (e3) (e1)) = (e0)) = ((op (op (e0) (e1)) (e1)) = (e0))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H40. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H29. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e3) (e1)) = (op (op (e0) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H41]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e0) (e1)) (e1)) = (op (op (e0) (e1)) (e1)))); [ zenon_intro zenon_H42 | zenon_intro zenon_H43 ]. % 1.08/1.30 cut (((op (op (e0) (e1)) (e1)) = (op (op (e0) (e1)) (e1))) = ((op (e3) (e1)) = (op (op (e0) (e1)) (e1)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H41. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H42. % 1.08/1.30 cut (((op (op (e0) (e1)) (e1)) = (op (op (e0) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H43]. % 1.08/1.30 cut (((op (op (e0) (e1)) (e1)) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H44]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e0) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H45 zenon_Hb). % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply zenon_H43. apply refl_equal. % 1.08/1.30 apply zenon_H43. apply refl_equal. % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H3f); [ zenon_intro zenon_H47 | zenon_intro zenon_H46 ]. % 1.08/1.30 cut (((op (e4) (e2)) = (e0)) = ((op (op (e0) (e2)) (e2)) = (e0))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H47. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H35. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e4) (e2)) = (op (op (e0) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H48]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e0) (e2)) (e2)) = (op (op (e0) (e2)) (e2)))); [ zenon_intro zenon_H49 | zenon_intro zenon_H4a ]. % 1.08/1.30 cut (((op (op (e0) (e2)) (e2)) = (op (op (e0) (e2)) (e2))) = ((op (e4) (e2)) = (op (op (e0) (e2)) (e2)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H48. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H49. % 1.08/1.30 cut (((op (op (e0) (e2)) (e2)) = (op (op (e0) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H4a]. % 1.08/1.30 cut (((op (op (e0) (e2)) (e2)) = (op (e4) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H4b]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.08/1.30 cut (((op (e0) (e2)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H4c zenon_Hd). % 1.08/1.30 apply zenon_H5. apply refl_equal. % 1.08/1.30 apply zenon_H4a. apply refl_equal. % 1.08/1.30 apply zenon_H4a. apply refl_equal. % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H46); [ zenon_intro zenon_H4e | zenon_intro zenon_H4d ]. % 1.08/1.30 cut (((op (e2) (e3)) = (e0)) = ((op (op (e0) (e3)) (e3)) = (e0))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H4e. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H23. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e2) (e3)) = (op (op (e0) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H4f]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e0) (e3)) (e3)) = (op (op (e0) (e3)) (e3)))); [ zenon_intro zenon_H50 | zenon_intro zenon_H51 ]. % 1.08/1.30 cut (((op (op (e0) (e3)) (e3)) = (op (op (e0) (e3)) (e3))) = ((op (e2) (e3)) = (op (op (e0) (e3)) (e3)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H4f. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H50. % 1.08/1.30 cut (((op (op (e0) (e3)) (e3)) = (op (op (e0) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H51]. % 1.08/1.30 cut (((op (op (e0) (e3)) (e3)) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H52]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.08/1.30 cut (((op (e0) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H53 zenon_Hf). % 1.08/1.30 apply zenon_H6. apply refl_equal. % 1.08/1.30 apply zenon_H51. apply refl_equal. % 1.08/1.30 apply zenon_H51. apply refl_equal. % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H55 | zenon_intro zenon_H54 ]. % 1.08/1.30 cut (((op (e1) (e4)) = (e0)) = ((op (op (e0) (e4)) (e4)) = (e0))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H55. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H1b. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e1) (e4)) = (op (op (e0) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H56]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e0) (e4)) (e4)) = (op (op (e0) (e4)) (e4)))); [ zenon_intro zenon_H57 | zenon_intro zenon_H58 ]. % 1.08/1.30 cut (((op (op (e0) (e4)) (e4)) = (op (op (e0) (e4)) (e4))) = ((op (e1) (e4)) = (op (op (e0) (e4)) (e4)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H56. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H57. % 1.08/1.30 cut (((op (op (e0) (e4)) (e4)) = (op (op (e0) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H58]. % 1.08/1.30 cut (((op (op (e0) (e4)) (e4)) = (op (e1) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H59]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.08/1.30 cut (((op (e0) (e4)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H5a zenon_H11). % 1.08/1.30 apply zenon_H7. apply refl_equal. % 1.08/1.30 apply zenon_H58. apply refl_equal. % 1.08/1.30 apply zenon_H58. apply refl_equal. % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H54); [ zenon_intro zenon_H5c | zenon_intro zenon_H5b ]. % 1.08/1.30 cut (((op (e2) (e0)) = (e1)) = ((op (op (e1) (e0)) (e0)) = (e1))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H5c. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H1d. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e2) (e0)) = (op (op (e1) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H5d]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e1) (e0)) (e0)) = (op (op (e1) (e0)) (e0)))); [ zenon_intro zenon_H5e | zenon_intro zenon_H5f ]. % 1.08/1.30 cut (((op (op (e1) (e0)) (e0)) = (op (op (e1) (e0)) (e0))) = ((op (e2) (e0)) = (op (op (e1) (e0)) (e0)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H5d. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H5e. % 1.08/1.30 cut (((op (op (e1) (e0)) (e0)) = (op (op (e1) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H5f]. % 1.08/1.30 cut (((op (op (e1) (e0)) (e0)) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H60]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e1) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H61 zenon_H13). % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply zenon_H5f. apply refl_equal. % 1.08/1.30 apply zenon_H5f. apply refl_equal. % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H5b); [ zenon_intro zenon_H63 | zenon_intro zenon_H62 ]. % 1.08/1.30 cut (((op (e1) (e1)) = (e1)) = ((op (op (e1) (e1)) (e1)) = (e1))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H63. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H15. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e1) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H64]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [ zenon_intro zenon_H65 | zenon_intro zenon_H66 ]. % 1.08/1.30 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1))) = ((op (e1) (e1)) = (op (op (e1) (e1)) (e1)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H64. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H65. % 1.08/1.30 cut (((op (op (e1) (e1)) (e1)) = (op (op (e1) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H66]. % 1.08/1.30 cut (((op (op (e1) (e1)) (e1)) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H67]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e1) (e1)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H68 zenon_H15). % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply zenon_H66. apply refl_equal. % 1.08/1.30 apply zenon_H66. apply refl_equal. % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H62); [ zenon_intro zenon_H6a | zenon_intro zenon_H69 ]. % 1.08/1.30 cut (((op (e3) (e2)) = (e1)) = ((op (op (e1) (e2)) (e2)) = (e1))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H6a. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H2b. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e3) (e2)) = (op (op (e1) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H6b]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e1) (e2)) (e2)) = (op (op (e1) (e2)) (e2)))); [ zenon_intro zenon_H6c | zenon_intro zenon_H6d ]. % 1.08/1.30 cut (((op (op (e1) (e2)) (e2)) = (op (op (e1) (e2)) (e2))) = ((op (e3) (e2)) = (op (op (e1) (e2)) (e2)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H6b. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H6c. % 1.08/1.30 cut (((op (op (e1) (e2)) (e2)) = (op (op (e1) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H6d]. % 1.08/1.30 cut (((op (op (e1) (e2)) (e2)) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H6e]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.08/1.30 cut (((op (e1) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6f]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H6f zenon_H17). % 1.08/1.30 apply zenon_H5. apply refl_equal. % 1.08/1.30 apply zenon_H6d. apply refl_equal. % 1.08/1.30 apply zenon_H6d. apply refl_equal. % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H69); [ zenon_intro zenon_H71 | zenon_intro zenon_H70 ]. % 1.08/1.30 cut (((op (e4) (e3)) = (e1)) = ((op (op (e1) (e3)) (e3)) = (e1))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H71. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H37. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e4) (e3)) = (op (op (e1) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H72]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e1) (e3)) (e3)) = (op (op (e1) (e3)) (e3)))); [ zenon_intro zenon_H73 | zenon_intro zenon_H74 ]. % 1.08/1.30 cut (((op (op (e1) (e3)) (e3)) = (op (op (e1) (e3)) (e3))) = ((op (e4) (e3)) = (op (op (e1) (e3)) (e3)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H72. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H73. % 1.08/1.30 cut (((op (op (e1) (e3)) (e3)) = (op (op (e1) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 1.08/1.30 cut (((op (op (e1) (e3)) (e3)) = (op (e4) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H75]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.08/1.30 cut (((op (e1) (e3)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H76]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H76 zenon_H19). % 1.08/1.30 apply zenon_H6. apply refl_equal. % 1.08/1.30 apply zenon_H74. apply refl_equal. % 1.08/1.30 apply zenon_H74. apply refl_equal. % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H70); [ zenon_intro zenon_H78 | zenon_intro zenon_H77 ]. % 1.08/1.30 cut (((op (e0) (e4)) = (e1)) = ((op (op (e1) (e4)) (e4)) = (e1))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H78. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H11. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e0) (e4)) = (op (op (e1) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H79]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e1) (e4)) (e4)) = (op (op (e1) (e4)) (e4)))); [ zenon_intro zenon_H7a | zenon_intro zenon_H7b ]. % 1.08/1.30 cut (((op (op (e1) (e4)) (e4)) = (op (op (e1) (e4)) (e4))) = ((op (e0) (e4)) = (op (op (e1) (e4)) (e4)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H79. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H7a. % 1.08/1.30 cut (((op (op (e1) (e4)) (e4)) = (op (op (e1) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H7b]. % 1.08/1.30 cut (((op (op (e1) (e4)) (e4)) = (op (e0) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H7c]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.08/1.30 cut (((op (e1) (e4)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H7d zenon_H1b). % 1.08/1.30 apply zenon_H7. apply refl_equal. % 1.08/1.30 apply zenon_H7b. apply refl_equal. % 1.08/1.30 apply zenon_H7b. apply refl_equal. % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H77); [ zenon_intro zenon_H7f | zenon_intro zenon_H7e ]. % 1.08/1.30 cut (((op (e1) (e0)) = (e2)) = ((op (op (e2) (e0)) (e0)) = (e2))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H7f. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H13. % 1.08/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.08/1.30 cut (((op (e1) (e0)) = (op (op (e2) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H80]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e2) (e0)) (e0)) = (op (op (e2) (e0)) (e0)))); [ zenon_intro zenon_H81 | zenon_intro zenon_H82 ]. % 1.08/1.30 cut (((op (op (e2) (e0)) (e0)) = (op (op (e2) (e0)) (e0))) = ((op (e1) (e0)) = (op (op (e2) (e0)) (e0)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H80. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H81. % 1.08/1.30 cut (((op (op (e2) (e0)) (e0)) = (op (op (e2) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H82]. % 1.08/1.30 cut (((op (op (e2) (e0)) (e0)) = (op (e1) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H83]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.08/1.30 cut (((op (e2) (e0)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H84]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H84 zenon_H1d). % 1.08/1.30 apply zenon_H3. apply refl_equal. % 1.08/1.30 apply zenon_H82. apply refl_equal. % 1.08/1.30 apply zenon_H82. apply refl_equal. % 1.08/1.30 apply zenon_H5. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H7e); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 1.08/1.30 cut (((op (e4) (e1)) = (e2)) = ((op (op (e2) (e1)) (e1)) = (e2))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H86. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H33. % 1.08/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.08/1.30 cut (((op (e4) (e1)) = (op (op (e2) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H87]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e2) (e1)) (e1)) = (op (op (e2) (e1)) (e1)))); [ zenon_intro zenon_H88 | zenon_intro zenon_H89 ]. % 1.08/1.30 cut (((op (op (e2) (e1)) (e1)) = (op (op (e2) (e1)) (e1))) = ((op (e4) (e1)) = (op (op (e2) (e1)) (e1)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H87. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H88. % 1.08/1.30 cut (((op (op (e2) (e1)) (e1)) = (op (op (e2) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H89]. % 1.08/1.30 cut (((op (op (e2) (e1)) (e1)) = (op (e4) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H8a]. % 1.08/1.30 congruence. % 1.08/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.08/1.30 cut (((op (e2) (e1)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 1.08/1.30 congruence. % 1.08/1.30 exact (zenon_H8b zenon_H1f). % 1.08/1.30 apply zenon_H4. apply refl_equal. % 1.08/1.30 apply zenon_H89. apply refl_equal. % 1.08/1.30 apply zenon_H89. apply refl_equal. % 1.08/1.30 apply zenon_H5. apply refl_equal. % 1.08/1.30 apply (zenon_notand_s _ _ zenon_H85); [ zenon_intro zenon_H8d | zenon_intro zenon_H8c ]. % 1.08/1.30 cut (((op (e2) (e2)) = (e2)) = ((op (op (e2) (e2)) (e2)) = (e2))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H8d. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H21. % 1.08/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.08/1.30 cut (((op (e2) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H8e]. % 1.08/1.30 congruence. % 1.08/1.30 elim (classic ((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [ zenon_intro zenon_H8f | zenon_intro zenon_H90 ]. % 1.08/1.30 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2))) = ((op (e2) (e2)) = (op (op (e2) (e2)) (e2)))). % 1.08/1.30 intro zenon_D_pnotp. % 1.08/1.30 apply zenon_H8e. % 1.08/1.30 rewrite <- zenon_D_pnotp. % 1.08/1.30 exact zenon_H8f. % 1.14/1.30 cut (((op (op (e2) (e2)) (e2)) = (op (op (e2) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H90]. % 1.14/1.30 cut (((op (op (e2) (e2)) (e2)) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H91]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e2) (e2)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H92]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H92 zenon_H21). % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply zenon_H90. apply refl_equal. % 1.14/1.30 apply zenon_H90. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H8c); [ zenon_intro zenon_H94 | zenon_intro zenon_H93 ]. % 1.14/1.30 cut (((op (e0) (e3)) = (e2)) = ((op (op (e2) (e3)) (e3)) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H94. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hf. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e0) (e3)) = (op (op (e2) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H95]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3)))); [ zenon_intro zenon_H96 | zenon_intro zenon_H97 ]. % 1.14/1.30 cut (((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3))) = ((op (e0) (e3)) = (op (op (e2) (e3)) (e3)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H95. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H96. % 1.14/1.30 cut (((op (op (e2) (e3)) (e3)) = (op (op (e2) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H97]. % 1.14/1.30 cut (((op (op (e2) (e3)) (e3)) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H98]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e2) (e3)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H99 zenon_H23). % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply zenon_H97. apply refl_equal. % 1.14/1.30 apply zenon_H97. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H93); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 1.14/1.30 cut (((op (e3) (e4)) = (e2)) = ((op (op (e2) (e4)) (e4)) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H9b. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2f. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e3) (e4)) = (op (op (e2) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H9c]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e4)) (e4)) = (op (op (e2) (e4)) (e4)))); [ zenon_intro zenon_H9d | zenon_intro zenon_H9e ]. % 1.14/1.30 cut (((op (op (e2) (e4)) (e4)) = (op (op (e2) (e4)) (e4))) = ((op (e3) (e4)) = (op (op (e2) (e4)) (e4)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H9c. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H9d. % 1.14/1.30 cut (((op (op (e2) (e4)) (e4)) = (op (op (e2) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H9e]. % 1.14/1.30 cut (((op (op (e2) (e4)) (e4)) = (op (e3) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H9f]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e2) (e4)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Ha0 zenon_H25). % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply zenon_H9e. apply refl_equal. % 1.14/1.30 apply zenon_H9e. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H9a); [ zenon_intro zenon_Ha2 | zenon_intro zenon_Ha1 ]. % 1.14/1.30 cut (((op (e4) (e0)) = (e3)) = ((op (op (e3) (e0)) (e0)) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Ha2. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H31. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e4) (e0)) = (op (op (e3) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Ha3]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e0)) (e0)) = (op (op (e3) (e0)) (e0)))); [ zenon_intro zenon_Ha4 | zenon_intro zenon_Ha5 ]. % 1.14/1.30 cut (((op (op (e3) (e0)) (e0)) = (op (op (e3) (e0)) (e0))) = ((op (e4) (e0)) = (op (op (e3) (e0)) (e0)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Ha3. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Ha4. % 1.14/1.30 cut (((op (op (e3) (e0)) (e0)) = (op (op (e3) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Ha5]. % 1.14/1.30 cut (((op (op (e3) (e0)) (e0)) = (op (e4) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Ha6]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e3) (e0)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Ha7 zenon_H27). % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply zenon_Ha5. apply refl_equal. % 1.14/1.30 apply zenon_Ha5. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Ha1); [ zenon_intro zenon_Ha9 | zenon_intro zenon_Ha8 ]. % 1.14/1.30 cut (((op (e0) (e1)) = (e3)) = ((op (op (e3) (e1)) (e1)) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Ha9. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hb. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e0) (e1)) = (op (op (e3) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Haa]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e1)) (e1)) = (op (op (e3) (e1)) (e1)))); [ zenon_intro zenon_Hab | zenon_intro zenon_Hac ]. % 1.14/1.30 cut (((op (op (e3) (e1)) (e1)) = (op (op (e3) (e1)) (e1))) = ((op (e0) (e1)) = (op (op (e3) (e1)) (e1)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Haa. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hab. % 1.14/1.30 cut (((op (op (e3) (e1)) (e1)) = (op (op (e3) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hac]. % 1.14/1.30 cut (((op (op (e3) (e1)) (e1)) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Had]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e3) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hae zenon_H29). % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply zenon_Hac. apply refl_equal. % 1.14/1.30 apply zenon_Hac. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Ha8); [ zenon_intro zenon_Hb0 | zenon_intro zenon_Haf ]. % 1.14/1.30 cut (((op (e1) (e2)) = (e3)) = ((op (op (e3) (e2)) (e2)) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hb0. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H17. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e1) (e2)) = (op (op (e3) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hb1]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2)))); [ zenon_intro zenon_Hb2 | zenon_intro zenon_Hb3 ]. % 1.14/1.30 cut (((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2))) = ((op (e1) (e2)) = (op (op (e3) (e2)) (e2)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hb1. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hb2. % 1.14/1.30 cut (((op (op (e3) (e2)) (e2)) = (op (op (e3) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hb3]. % 1.14/1.30 cut (((op (op (e3) (e2)) (e2)) = (op (e1) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hb4]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e3) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hb5 zenon_H2b). % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply zenon_Hb3. apply refl_equal. % 1.14/1.30 apply zenon_Hb3. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Haf); [ zenon_intro zenon_Hb7 | zenon_intro zenon_Hb6 ]. % 1.14/1.30 cut (((op (e3) (e3)) = (e3)) = ((op (op (e3) (e3)) (e3)) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hb7. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2d. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e3) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hb8]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [ zenon_intro zenon_Hb9 | zenon_intro zenon_Hba ]. % 1.14/1.30 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3))) = ((op (e3) (e3)) = (op (op (e3) (e3)) (e3)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hb8. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hb9. % 1.14/1.30 cut (((op (op (e3) (e3)) (e3)) = (op (op (e3) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hba]. % 1.14/1.30 cut (((op (op (e3) (e3)) (e3)) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hbb]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e3) (e3)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hbc zenon_H2d). % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply zenon_Hba. apply refl_equal. % 1.14/1.30 apply zenon_Hba. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hb6); [ zenon_intro zenon_Hbe | zenon_intro zenon_Hbd ]. % 1.14/1.30 cut (((op (e2) (e4)) = (e3)) = ((op (op (e3) (e4)) (e4)) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hbe. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H25. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e2) (e4)) = (op (op (e3) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_Hbf]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e4)) (e4)) = (op (op (e3) (e4)) (e4)))); [ zenon_intro zenon_Hc0 | zenon_intro zenon_Hc1 ]. % 1.14/1.30 cut (((op (op (e3) (e4)) (e4)) = (op (op (e3) (e4)) (e4))) = ((op (e2) (e4)) = (op (op (e3) (e4)) (e4)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hbf. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hc0. % 1.14/1.30 cut (((op (op (e3) (e4)) (e4)) = (op (op (e3) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_Hc1]. % 1.14/1.30 cut (((op (op (e3) (e4)) (e4)) = (op (e2) (e4)))); [idtac | apply NNPP; zenon_intro zenon_Hc2]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e3) (e4)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hc3 zenon_H2f). % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply zenon_Hc1. apply refl_equal. % 1.14/1.30 apply zenon_Hc1. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hbd); [ zenon_intro zenon_Hc5 | zenon_intro zenon_Hc4 ]. % 1.14/1.30 cut (((op (e3) (e0)) = (e4)) = ((op (op (e4) (e0)) (e0)) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hc5. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H27. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e3) (e0)) = (op (op (e4) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Hc6]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e0)) (e0)) = (op (op (e4) (e0)) (e0)))); [ zenon_intro zenon_Hc7 | zenon_intro zenon_Hc8 ]. % 1.14/1.30 cut (((op (op (e4) (e0)) (e0)) = (op (op (e4) (e0)) (e0))) = ((op (e3) (e0)) = (op (op (e4) (e0)) (e0)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hc6. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hc7. % 1.14/1.30 cut (((op (op (e4) (e0)) (e0)) = (op (op (e4) (e0)) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Hc8]. % 1.14/1.30 cut (((op (op (e4) (e0)) (e0)) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_Hc9]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e4) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hca zenon_H31). % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply zenon_Hc8. apply refl_equal. % 1.14/1.30 apply zenon_Hc8. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hc4); [ zenon_intro zenon_Hcc | zenon_intro zenon_Hcb ]. % 1.14/1.30 cut (((op (e2) (e1)) = (e4)) = ((op (op (e4) (e1)) (e1)) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hcc. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H1f. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e2) (e1)) = (op (op (e4) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hcd]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e1)) (e1)) = (op (op (e4) (e1)) (e1)))); [ zenon_intro zenon_Hce | zenon_intro zenon_Hcf ]. % 1.14/1.30 cut (((op (op (e4) (e1)) (e1)) = (op (op (e4) (e1)) (e1))) = ((op (e2) (e1)) = (op (op (e4) (e1)) (e1)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hcd. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hce. % 1.14/1.30 cut (((op (op (e4) (e1)) (e1)) = (op (op (e4) (e1)) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hcf]. % 1.14/1.30 cut (((op (op (e4) (e1)) (e1)) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_Hd0]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e4) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hd1 zenon_H33). % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply zenon_Hcf. apply refl_equal. % 1.14/1.30 apply zenon_Hcf. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hcb); [ zenon_intro zenon_Hd3 | zenon_intro zenon_Hd2 ]. % 1.14/1.30 cut (((op (e0) (e2)) = (e4)) = ((op (op (e4) (e2)) (e2)) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hd3. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hd. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e0) (e2)) = (op (op (e4) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hd4]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e2)) (e2)) = (op (op (e4) (e2)) (e2)))); [ zenon_intro zenon_Hd5 | zenon_intro zenon_Hd6 ]. % 1.14/1.30 cut (((op (op (e4) (e2)) (e2)) = (op (op (e4) (e2)) (e2))) = ((op (e0) (e2)) = (op (op (e4) (e2)) (e2)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hd4. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hd5. % 1.14/1.30 cut (((op (op (e4) (e2)) (e2)) = (op (op (e4) (e2)) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hd6]. % 1.14/1.30 cut (((op (op (e4) (e2)) (e2)) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_Hd7]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e4) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hd8 zenon_H35). % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply zenon_Hd6. apply refl_equal. % 1.14/1.30 apply zenon_Hd6. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hd2); [ zenon_intro zenon_Hda | zenon_intro zenon_Hd9 ]. % 1.14/1.30 cut (((op (e1) (e3)) = (e4)) = ((op (op (e4) (e3)) (e3)) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hda. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H19. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e1) (e3)) = (op (op (e4) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hdb]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e3)) (e3)) = (op (op (e4) (e3)) (e3)))); [ zenon_intro zenon_Hdc | zenon_intro zenon_Hdd ]. % 1.14/1.30 cut (((op (op (e4) (e3)) (e3)) = (op (op (e4) (e3)) (e3))) = ((op (e1) (e3)) = (op (op (e4) (e3)) (e3)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_Hdb. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hdc. % 1.14/1.30 cut (((op (op (e4) (e3)) (e3)) = (op (op (e4) (e3)) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hdd]. % 1.14/1.30 cut (((op (op (e4) (e3)) (e3)) = (op (e1) (e3)))); [idtac | apply NNPP; zenon_intro zenon_Hde]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e4) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hdf]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hdf zenon_H37). % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply zenon_Hdd. apply refl_equal. % 1.14/1.30 apply zenon_Hdd. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hd9); [ zenon_intro zenon_He1 | zenon_intro zenon_He0 ]. % 1.14/1.30 cut (((op (e4) (e4)) = (e4)) = ((op (op (e4) (e4)) (e4)) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_He1. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H36. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e4) (e4)) = (op (op (e4) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_He2]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e4)) (e4)) = (op (op (e4) (e4)) (e4)))); [ zenon_intro zenon_He3 | zenon_intro zenon_He4 ]. % 1.14/1.30 cut (((op (op (e4) (e4)) (e4)) = (op (op (e4) (e4)) (e4))) = ((op (e4) (e4)) = (op (op (e4) (e4)) (e4)))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_He2. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_He3. % 1.14/1.30 cut (((op (op (e4) (e4)) (e4)) = (op (op (e4) (e4)) (e4)))); [idtac | apply NNPP; zenon_intro zenon_He4]. % 1.14/1.30 cut (((op (op (e4) (e4)) (e4)) = (op (e4) (e4)))); [idtac | apply NNPP; zenon_intro zenon_He5]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e4) (e4)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_He6 zenon_H36). % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply zenon_He4. apply refl_equal. % 1.14/1.30 apply zenon_He4. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_He0); [ zenon_intro zenon_He8 | zenon_intro zenon_He7 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_He8). zenon_intro zenon_H3e. zenon_intro zenon_He9. % 1.14/1.30 exact (zenon_H3e zenon_H9). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_He7); [ zenon_intro zenon_Heb | zenon_intro zenon_Hea ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Heb). zenon_intro zenon_Hed. zenon_intro zenon_Hec. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hec). zenon_intro zenon_Hef. zenon_intro zenon_Hee. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hee). zenon_intro zenon_Hf1. zenon_intro zenon_Hf0. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hf0). zenon_intro zenon_H45. zenon_intro zenon_Hf2. % 1.14/1.30 exact (zenon_H45 zenon_Hb). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hea); [ zenon_intro zenon_Hf4 | zenon_intro zenon_Hf3 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hf4). zenon_intro zenon_Hf6. zenon_intro zenon_Hf5. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hf5). zenon_intro zenon_Hf8. zenon_intro zenon_Hf7. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hf7). zenon_intro zenon_Hfa. zenon_intro zenon_Hf9. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hf9). zenon_intro zenon_Hfb. zenon_intro zenon_H4c. % 1.14/1.30 exact (zenon_H4c zenon_Hd). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hf3); [ zenon_intro zenon_Hfd | zenon_intro zenon_Hfc ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hfd). zenon_intro zenon_Hff. zenon_intro zenon_Hfe. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_Hfe). zenon_intro zenon_H101. zenon_intro zenon_H100. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H100). zenon_intro zenon_H53. zenon_intro zenon_H102. % 1.14/1.30 exact (zenon_H53 zenon_Hf). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_Hfc); [ zenon_intro zenon_H104 | zenon_intro zenon_H103 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H104). zenon_intro zenon_H106. zenon_intro zenon_H105. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H105). zenon_intro zenon_H5a. zenon_intro zenon_H107. % 1.14/1.30 exact (zenon_H5a zenon_H11). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H103); [ zenon_intro zenon_H109 | zenon_intro zenon_H108 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H109). zenon_intro zenon_H10b. zenon_intro zenon_H10a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H10a). zenon_intro zenon_H10d. zenon_intro zenon_H10c. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H10c). zenon_intro zenon_H61. zenon_intro zenon_H10e. % 1.14/1.30 exact (zenon_H61 zenon_H13). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H108); [ zenon_intro zenon_H110 | zenon_intro zenon_H10f ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H110). zenon_intro zenon_H112. zenon_intro zenon_H111. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H111). zenon_intro zenon_H68. zenon_intro zenon_H113. % 1.14/1.30 exact (zenon_H68 zenon_H15). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H10f); [ zenon_intro zenon_H115 | zenon_intro zenon_H114 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H115). zenon_intro zenon_H117. zenon_intro zenon_H116. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H116). zenon_intro zenon_H119. zenon_intro zenon_H118. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H118). zenon_intro zenon_H11b. zenon_intro zenon_H11a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H11a). zenon_intro zenon_H6f. zenon_intro zenon_H11c. % 1.14/1.30 exact (zenon_H6f zenon_H17). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H114); [ zenon_intro zenon_H11e | zenon_intro zenon_H11d ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H11e). zenon_intro zenon_H120. zenon_intro zenon_H11f. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H11f). zenon_intro zenon_H122. zenon_intro zenon_H121. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H121). zenon_intro zenon_H124. zenon_intro zenon_H123. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H123). zenon_intro zenon_H125. zenon_intro zenon_H76. % 1.14/1.30 exact (zenon_H76 zenon_H19). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H11d); [ zenon_intro zenon_H127 | zenon_intro zenon_H126 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H127). zenon_intro zenon_H7d. zenon_intro zenon_H128. % 1.14/1.30 exact (zenon_H7d zenon_H1b). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H126); [ zenon_intro zenon_H12a | zenon_intro zenon_H129 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H12a). zenon_intro zenon_H12c. zenon_intro zenon_H12b. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H12b). zenon_intro zenon_H84. zenon_intro zenon_H12d. % 1.14/1.30 exact (zenon_H84 zenon_H1d). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H129); [ zenon_intro zenon_H12f | zenon_intro zenon_H12e ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H12f). zenon_intro zenon_H131. zenon_intro zenon_H130. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H130). zenon_intro zenon_H133. zenon_intro zenon_H132. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H132). zenon_intro zenon_H135. zenon_intro zenon_H134. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H134). zenon_intro zenon_H136. zenon_intro zenon_H8b. % 1.14/1.30 exact (zenon_H8b zenon_H1f). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H12e); [ zenon_intro zenon_H138 | zenon_intro zenon_H137 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H138). zenon_intro zenon_H13a. zenon_intro zenon_H139. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H139). zenon_intro zenon_H13c. zenon_intro zenon_H13b. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H13b). zenon_intro zenon_H92. zenon_intro zenon_H13d. % 1.14/1.30 exact (zenon_H92 zenon_H21). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H137); [ zenon_intro zenon_H13f | zenon_intro zenon_H13e ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H13f). zenon_intro zenon_H99. zenon_intro zenon_H140. % 1.14/1.30 exact (zenon_H99 zenon_H23). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H13e); [ zenon_intro zenon_H142 | zenon_intro zenon_H141 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H142). zenon_intro zenon_H144. zenon_intro zenon_H143. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H143). zenon_intro zenon_H146. zenon_intro zenon_H145. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H145). zenon_intro zenon_H148. zenon_intro zenon_H147. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H147). zenon_intro zenon_Ha0. zenon_intro zenon_H149. % 1.14/1.30 exact (zenon_Ha0 zenon_H25). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H141); [ zenon_intro zenon_H14b | zenon_intro zenon_H14a ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H14b). zenon_intro zenon_H14d. zenon_intro zenon_H14c. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H14c). zenon_intro zenon_H14f. zenon_intro zenon_H14e. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H14e). zenon_intro zenon_H151. zenon_intro zenon_H150. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H150). zenon_intro zenon_H152. zenon_intro zenon_Ha7. % 1.14/1.30 exact (zenon_Ha7 zenon_H27). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H14a); [ zenon_intro zenon_H154 | zenon_intro zenon_H153 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H154). zenon_intro zenon_Hae. zenon_intro zenon_H155. % 1.14/1.30 exact (zenon_Hae zenon_H29). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H153); [ zenon_intro zenon_H157 | zenon_intro zenon_H156 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H157). zenon_intro zenon_H159. zenon_intro zenon_H158. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H158). zenon_intro zenon_Hb5. zenon_intro zenon_H15a. % 1.14/1.30 exact (zenon_Hb5 zenon_H2b). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H156); [ zenon_intro zenon_H15c | zenon_intro zenon_H15b ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H15c). zenon_intro zenon_H15e. zenon_intro zenon_H15d. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H15d). zenon_intro zenon_H160. zenon_intro zenon_H15f. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H15f). zenon_intro zenon_H162. zenon_intro zenon_H161. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H161). zenon_intro zenon_Hbc. zenon_intro zenon_H163. % 1.14/1.30 exact (zenon_Hbc zenon_H2d). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H15b); [ zenon_intro zenon_H165 | zenon_intro zenon_H164 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H165). zenon_intro zenon_H167. zenon_intro zenon_H166. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H166). zenon_intro zenon_H169. zenon_intro zenon_H168. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H168). zenon_intro zenon_Hc3. zenon_intro zenon_H16a. % 1.14/1.30 exact (zenon_Hc3 zenon_H2f). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H164); [ zenon_intro zenon_H16c | zenon_intro zenon_H16b ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H16c). zenon_intro zenon_H16e. zenon_intro zenon_H16d. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H16d). zenon_intro zenon_H170. zenon_intro zenon_H16f. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H16f). zenon_intro zenon_H172. zenon_intro zenon_H171. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H171). zenon_intro zenon_Hca. zenon_intro zenon_H173. % 1.14/1.30 exact (zenon_Hca zenon_H31). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H16b); [ zenon_intro zenon_H175 | zenon_intro zenon_H174 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H175). zenon_intro zenon_H177. zenon_intro zenon_H176. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H176). zenon_intro zenon_H179. zenon_intro zenon_H178. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H178). zenon_intro zenon_Hd1. zenon_intro zenon_H17a. % 1.14/1.30 exact (zenon_Hd1 zenon_H33). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H174); [ zenon_intro zenon_H17c | zenon_intro zenon_H17b ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H17c). zenon_intro zenon_Hd8. zenon_intro zenon_H17d. % 1.14/1.30 exact (zenon_Hd8 zenon_H35). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H17b); [ zenon_intro zenon_H17f | zenon_intro zenon_H17e ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H17f). zenon_intro zenon_H181. zenon_intro zenon_H180. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H180). zenon_intro zenon_Hdf. zenon_intro zenon_H182. % 1.14/1.30 exact (zenon_Hdf zenon_H37). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H17e); [ zenon_intro zenon_H184 | zenon_intro zenon_H183 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H184). zenon_intro zenon_H186. zenon_intro zenon_H185. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H185). zenon_intro zenon_H188. zenon_intro zenon_H187. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H187). zenon_intro zenon_H18a. zenon_intro zenon_H189. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H189). zenon_intro zenon_H18b. zenon_intro zenon_He6. % 1.14/1.30 exact (zenon_He6 zenon_H36). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H183); [ zenon_intro zenon_H18d | zenon_intro zenon_H18c ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H18d). zenon_intro zenon_H3e. zenon_intro zenon_H18e. % 1.14/1.30 exact (zenon_H3e zenon_H9). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H18c); [ zenon_intro zenon_H190 | zenon_intro zenon_H18f ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H190). zenon_intro zenon_H3e. zenon_intro zenon_H191. % 1.14/1.30 exact (zenon_H3e zenon_H9). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H18f); [ zenon_intro zenon_H193 | zenon_intro zenon_H192 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H193). zenon_intro zenon_H195. zenon_intro zenon_H194. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H194). zenon_intro zenon_Hef. zenon_intro zenon_H196. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H196). zenon_intro zenon_Hf8. zenon_intro zenon_H197. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H197). zenon_intro zenon_H101. zenon_intro zenon_H5a. % 1.14/1.30 exact (zenon_H5a zenon_H11). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H192); [ zenon_intro zenon_H199 | zenon_intro zenon_H198 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H199). zenon_intro zenon_H195. zenon_intro zenon_H19a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H19a). zenon_intro zenon_H10d. zenon_intro zenon_H19b. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H19b). zenon_intro zenon_H84. zenon_intro zenon_H19c. % 1.14/1.30 exact (zenon_H84 zenon_H1d). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H198); [ zenon_intro zenon_H19e | zenon_intro zenon_H19d ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H19e). zenon_intro zenon_H1a0. zenon_intro zenon_H19f. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H19f). zenon_intro zenon_Hf1. zenon_intro zenon_H1a1. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1a1). zenon_intro zenon_Hfa. zenon_intro zenon_H1a2. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1a2). zenon_intro zenon_H53. zenon_intro zenon_H1a3. % 1.14/1.30 exact (zenon_H53 zenon_Hf). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H19d); [ zenon_intro zenon_H1a5 | zenon_intro zenon_H1a4 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1a5). zenon_intro zenon_H1a0. zenon_intro zenon_H1a6. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1a6). zenon_intro zenon_H61. zenon_intro zenon_H1a7. % 1.14/1.30 exact (zenon_H61 zenon_H13). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1a4); [ zenon_intro zenon_H1a9 | zenon_intro zenon_H1a8 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1a9). zenon_intro zenon_H1ab. zenon_intro zenon_H1aa. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1aa). zenon_intro zenon_H45. zenon_intro zenon_H1ac. % 1.14/1.30 exact (zenon_H45 zenon_Hb). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1a8); [ zenon_intro zenon_H1ae | zenon_intro zenon_H1ad ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1ae). zenon_intro zenon_H1ab. zenon_intro zenon_H1af. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1af). zenon_intro zenon_H1b1. zenon_intro zenon_H1b0. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1b0). zenon_intro zenon_H1b3. zenon_intro zenon_H1b2. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1b2). zenon_intro zenon_H152. zenon_intro zenon_Hca. % 1.14/1.30 exact (zenon_Hca zenon_H31). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1ad); [ zenon_intro zenon_H1b5 | zenon_intro zenon_H1b4 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1b5). zenon_intro zenon_H1b7. zenon_intro zenon_H1b6. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1b6). zenon_intro zenon_Hf2. zenon_intro zenon_H1b8. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1b8). zenon_intro zenon_H4c. zenon_intro zenon_H1b9. % 1.14/1.30 exact (zenon_H4c zenon_Hd). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1b4); [ zenon_intro zenon_H1bb | zenon_intro zenon_H1ba ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1bb). zenon_intro zenon_H1b7. zenon_intro zenon_H1bc. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1bc). zenon_intro zenon_H1be. zenon_intro zenon_H1bd. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1bd). zenon_intro zenon_H1c0. zenon_intro zenon_H1bf. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1bf). zenon_intro zenon_Ha7. zenon_intro zenon_H173. % 1.14/1.30 exact (zenon_Ha7 zenon_H27). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1ba); [ zenon_intro zenon_H1c2 | zenon_intro zenon_H1c1 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c2). zenon_intro zenon_H10b. zenon_intro zenon_H1c3. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c3). zenon_intro zenon_H112. zenon_intro zenon_H1c4. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c4). zenon_intro zenon_H117. zenon_intro zenon_H1c5. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c5). zenon_intro zenon_H120. zenon_intro zenon_H7d. % 1.14/1.30 exact (zenon_H7d zenon_H1b). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1c1); [ zenon_intro zenon_H1c7 | zenon_intro zenon_H1c6 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c7). zenon_intro zenon_Hed. zenon_intro zenon_H1c8. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c8). zenon_intro zenon_H112. zenon_intro zenon_H1c9. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1c9). zenon_intro zenon_H131. zenon_intro zenon_H1ca. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1ca). zenon_intro zenon_Hae. zenon_intro zenon_H177. % 1.14/1.30 exact (zenon_Hae zenon_H29). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1c6); [ zenon_intro zenon_H1cc | zenon_intro zenon_H1cb ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1cc). zenon_intro zenon_H10d. zenon_intro zenon_H1cd. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1cd). zenon_intro zenon_H68. zenon_intro zenon_H1ce. % 1.14/1.30 exact (zenon_H68 zenon_H15). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1cb); [ zenon_intro zenon_H1d0 | zenon_intro zenon_H1cf ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1d0). zenon_intro zenon_Hef. zenon_intro zenon_H1d1. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1d1). zenon_intro zenon_H68. zenon_intro zenon_H1d2. % 1.14/1.30 exact (zenon_H68 zenon_H15). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1cf); [ zenon_intro zenon_H1d4 | zenon_intro zenon_H1d3 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1d4). zenon_intro zenon_H61. zenon_intro zenon_H1d5. % 1.14/1.30 exact (zenon_H61 zenon_H13). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1d3); [ zenon_intro zenon_H1d7 | zenon_intro zenon_H1d6 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1d7). zenon_intro zenon_Hf1. zenon_intro zenon_H1d8. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1d8). zenon_intro zenon_H1da. zenon_intro zenon_H1d9. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1d9). zenon_intro zenon_H135. zenon_intro zenon_H1db. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1db). zenon_intro zenon_H1dc. zenon_intro zenon_Hd1. % 1.14/1.30 exact (zenon_Hd1 zenon_H33). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1d6); [ zenon_intro zenon_H1de | zenon_intro zenon_H1dd ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1de). zenon_intro zenon_H1b1. zenon_intro zenon_H1df. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1df). zenon_intro zenon_H1e1. zenon_intro zenon_H1e0. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1e0). zenon_intro zenon_H6f. zenon_intro zenon_H1e2. % 1.14/1.30 exact (zenon_H6f zenon_H17). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1dd); [ zenon_intro zenon_H1e4 | zenon_intro zenon_H1e3 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1e4). zenon_intro zenon_H45. zenon_intro zenon_H1e5. % 1.14/1.30 exact (zenon_H45 zenon_Hb). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1e3); [ zenon_intro zenon_H1e7 | zenon_intro zenon_H1e6 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1e7). zenon_intro zenon_H1be. zenon_intro zenon_H1e8. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1e8). zenon_intro zenon_H1ea. zenon_intro zenon_H1e9. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1e9). zenon_intro zenon_H11c. zenon_intro zenon_H1eb. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1eb). zenon_intro zenon_H76. zenon_intro zenon_H1ec. % 1.14/1.30 exact (zenon_H76 zenon_H19). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1e6); [ zenon_intro zenon_H1ee | zenon_intro zenon_H1ed ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1ee). zenon_intro zenon_Hf2. zenon_intro zenon_H1ef. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1ef). zenon_intro zenon_H1ea. zenon_intro zenon_H1f0. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f0). zenon_intro zenon_H8b. zenon_intro zenon_H1f1. % 1.14/1.30 exact (zenon_H8b zenon_H1f). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1ed); [ zenon_intro zenon_H1f3 | zenon_intro zenon_H1f2 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f3). zenon_intro zenon_H12c. zenon_intro zenon_H1f4. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f4). zenon_intro zenon_H131. zenon_intro zenon_H1f5. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f5). zenon_intro zenon_H13a. zenon_intro zenon_H1f6. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f6). zenon_intro zenon_H99. zenon_intro zenon_H144. % 1.14/1.30 exact (zenon_H99 zenon_H23). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1f2); [ zenon_intro zenon_H1f8 | zenon_intro zenon_H1f7 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f8). zenon_intro zenon_Hf6. zenon_intro zenon_H1f9. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1f9). zenon_intro zenon_H117. zenon_intro zenon_H1fa. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1fa). zenon_intro zenon_H13a. zenon_intro zenon_H1fb. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1fb). zenon_intro zenon_H159. zenon_intro zenon_Hd8. % 1.14/1.30 exact (zenon_Hd8 zenon_H35). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1f7); [ zenon_intro zenon_H1fd | zenon_intro zenon_H1fc ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H1fd). zenon_intro zenon_H84. zenon_intro zenon_H1fe. % 1.14/1.30 exact (zenon_H84 zenon_H1d). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1fc); [ zenon_intro zenon_H200 | zenon_intro zenon_H1ff ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H200). zenon_intro zenon_Hf8. zenon_intro zenon_H201. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H201). zenon_intro zenon_H119. zenon_intro zenon_H202. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H202). zenon_intro zenon_H13c. zenon_intro zenon_H203. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H203). zenon_intro zenon_Hb5. zenon_intro zenon_H204. % 1.14/1.30 exact (zenon_Hb5 zenon_H2b). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H1ff); [ zenon_intro zenon_H206 | zenon_intro zenon_H205 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H206). zenon_intro zenon_H208. zenon_intro zenon_H207. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H207). zenon_intro zenon_H135. zenon_intro zenon_H209. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H209). zenon_intro zenon_H92. zenon_intro zenon_H20a. % 1.14/1.30 exact (zenon_H92 zenon_H21). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H205); [ zenon_intro zenon_H20c | zenon_intro zenon_H20b ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H20c). zenon_intro zenon_Hfa. zenon_intro zenon_H20d. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H20d). zenon_intro zenon_H11b. zenon_intro zenon_H20e. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H20e). zenon_intro zenon_H92. zenon_intro zenon_H20f. % 1.14/1.30 exact (zenon_H92 zenon_H21). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H20b); [ zenon_intro zenon_H211 | zenon_intro zenon_H210 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H211). zenon_intro zenon_H1b3. zenon_intro zenon_H212. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H212). zenon_intro zenon_H136. zenon_intro zenon_H213. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H213). zenon_intro zenon_H215. zenon_intro zenon_H214. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H214). zenon_intro zenon_H216. zenon_intro zenon_Ha0. % 1.14/1.30 exact (zenon_Ha0 zenon_H25). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H210); [ zenon_intro zenon_H218 | zenon_intro zenon_H217 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H218). zenon_intro zenon_Hfb. zenon_intro zenon_H219. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H219). zenon_intro zenon_H6f. zenon_intro zenon_H21a. % 1.14/1.30 exact (zenon_H6f zenon_H17). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H217); [ zenon_intro zenon_H21c | zenon_intro zenon_H21b ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H21c). zenon_intro zenon_H1c0. zenon_intro zenon_H21d. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H21d). zenon_intro zenon_H8b. zenon_intro zenon_H21e. % 1.14/1.30 exact (zenon_H8b zenon_H1f). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H21b); [ zenon_intro zenon_H220 | zenon_intro zenon_H21f ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H220). zenon_intro zenon_H4c. zenon_intro zenon_H221. % 1.14/1.30 exact (zenon_H4c zenon_Hd). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H21f); [ zenon_intro zenon_H223 | zenon_intro zenon_H222 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H223). zenon_intro zenon_H14d. zenon_intro zenon_H224. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H224). zenon_intro zenon_Hae. zenon_intro zenon_H225. % 1.14/1.30 exact (zenon_Hae zenon_H29). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H222); [ zenon_intro zenon_H227 | zenon_intro zenon_H226 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H227). zenon_intro zenon_Hff. zenon_intro zenon_H228. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H228). zenon_intro zenon_H120. zenon_intro zenon_H229. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H229). zenon_intro zenon_H99. zenon_intro zenon_H22a. % 1.14/1.30 exact (zenon_H99 zenon_H23). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H226); [ zenon_intro zenon_H22c | zenon_intro zenon_H22b ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H22c). zenon_intro zenon_H14f. zenon_intro zenon_H22d. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H22d). zenon_intro zenon_H22f. zenon_intro zenon_H22e. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H22e). zenon_intro zenon_Hb5. zenon_intro zenon_H230. % 1.14/1.30 exact (zenon_Hb5 zenon_H2b). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H22b); [ zenon_intro zenon_H232 | zenon_intro zenon_H231 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H232). zenon_intro zenon_H101. zenon_intro zenon_H233. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H233). zenon_intro zenon_H122. zenon_intro zenon_H234. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H234). zenon_intro zenon_H236. zenon_intro zenon_H235. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H235). zenon_intro zenon_H160. zenon_intro zenon_Hdf. % 1.14/1.30 exact (zenon_Hdf zenon_H37). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H231); [ zenon_intro zenon_H238 | zenon_intro zenon_H237 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H238). zenon_intro zenon_H151. zenon_intro zenon_H239. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H239). zenon_intro zenon_H1dc. zenon_intro zenon_H23a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H23a). zenon_intro zenon_H23c. zenon_intro zenon_H23b. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H23b). zenon_intro zenon_H162. zenon_intro zenon_Hc3. % 1.14/1.30 exact (zenon_Hc3 zenon_H2f). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H237); [ zenon_intro zenon_H23e | zenon_intro zenon_H23d ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H23e). zenon_intro zenon_H53. zenon_intro zenon_H23f. % 1.14/1.30 exact (zenon_H53 zenon_Hf). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H23d); [ zenon_intro zenon_H241 | zenon_intro zenon_H240 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H241). zenon_intro zenon_H152. zenon_intro zenon_H242. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H242). zenon_intro zenon_H244. zenon_intro zenon_H243. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H243). zenon_intro zenon_H246. zenon_intro zenon_H245. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H245). zenon_intro zenon_Hbc. zenon_intro zenon_H247. % 1.14/1.30 exact (zenon_Hbc zenon_H2d). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H240); [ zenon_intro zenon_H249 | zenon_intro zenon_H248 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H249). zenon_intro zenon_H24b. zenon_intro zenon_H24a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H24a). zenon_intro zenon_H125. zenon_intro zenon_H24c. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H24c). zenon_intro zenon_H216. zenon_intro zenon_H24d. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H24d). zenon_intro zenon_Hbc. zenon_intro zenon_H24e. % 1.14/1.30 exact (zenon_Hbc zenon_H2d). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H248); [ zenon_intro zenon_H250 | zenon_intro zenon_H24f ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H250). zenon_intro zenon_Ha7. zenon_intro zenon_H251. % 1.14/1.30 exact (zenon_Ha7 zenon_H27). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H24f); [ zenon_intro zenon_H253 | zenon_intro zenon_H252 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H253). zenon_intro zenon_H255. zenon_intro zenon_H254. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H254). zenon_intro zenon_H76. zenon_intro zenon_H256. % 1.14/1.30 exact (zenon_H76 zenon_H19). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H252); [ zenon_intro zenon_H258 | zenon_intro zenon_H257 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H258). zenon_intro zenon_H16e. zenon_intro zenon_H259. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H259). zenon_intro zenon_H177. zenon_intro zenon_H25a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H25a). zenon_intro zenon_Hd8. zenon_intro zenon_H25b. % 1.14/1.30 exact (zenon_Hd8 zenon_H35). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H257); [ zenon_intro zenon_H25d | zenon_intro zenon_H25c ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H25d). zenon_intro zenon_H106. zenon_intro zenon_H25e. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H25e). zenon_intro zenon_H7d. zenon_intro zenon_H25f. % 1.14/1.30 exact (zenon_H7d zenon_H1b). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H25c); [ zenon_intro zenon_H261 | zenon_intro zenon_H260 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H261). zenon_intro zenon_H170. zenon_intro zenon_H262. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H262). zenon_intro zenon_H179. zenon_intro zenon_H263. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H263). zenon_intro zenon_H204. zenon_intro zenon_H264. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H264). zenon_intro zenon_Hdf. zenon_intro zenon_H188. % 1.14/1.30 exact (zenon_Hdf zenon_H37). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H260); [ zenon_intro zenon_H266 | zenon_intro zenon_H265 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H266). zenon_intro zenon_H5a. zenon_intro zenon_H267. % 1.14/1.30 exact (zenon_H5a zenon_H11). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H265); [ zenon_intro zenon_H269 | zenon_intro zenon_H268 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H269). zenon_intro zenon_H172. zenon_intro zenon_H26a. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H26a). zenon_intro zenon_Hd1. zenon_intro zenon_H26b. % 1.14/1.30 exact (zenon_Hd1 zenon_H33). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H268); [ zenon_intro zenon_H26d | zenon_intro zenon_H26c ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H26d). zenon_intro zenon_H1a3. zenon_intro zenon_H26e. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H26e). zenon_intro zenon_H270. zenon_intro zenon_H26f. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H26f). zenon_intro zenon_H148. zenon_intro zenon_H271. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H271). zenon_intro zenon_Hc3. zenon_intro zenon_H18a. % 1.14/1.30 exact (zenon_Hc3 zenon_H2f). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H26c); [ zenon_intro zenon_H273 | zenon_intro zenon_H272 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H273). zenon_intro zenon_Hca. zenon_intro zenon_H274. % 1.14/1.30 exact (zenon_Hca zenon_H31). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H272); [ zenon_intro zenon_H276 | zenon_intro zenon_H275 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H276). zenon_intro zenon_H278. zenon_intro zenon_H277. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H277). zenon_intro zenon_H27a. zenon_intro zenon_H279. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H279). zenon_intro zenon_Ha0. zenon_intro zenon_H27b. % 1.14/1.30 exact (zenon_Ha0 zenon_H25). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H275); [ zenon_intro zenon_H27d | zenon_intro zenon_H27c ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H27d). zenon_intro zenon_H173. zenon_intro zenon_H27e. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H27e). zenon_intro zenon_H280. zenon_intro zenon_H27f. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H27f). zenon_intro zenon_H282. zenon_intro zenon_H281. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H281). zenon_intro zenon_H283. zenon_intro zenon_He6. % 1.14/1.30 exact (zenon_He6 zenon_H36). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H27c); [ zenon_intro zenon_H285 | zenon_intro zenon_H284 ]. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H285). zenon_intro zenon_H287. zenon_intro zenon_H286. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H286). zenon_intro zenon_H1ec. zenon_intro zenon_H288. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H288). zenon_intro zenon_H149. zenon_intro zenon_H289. % 1.14/1.30 apply (zenon_notor_s _ _ zenon_H289). zenon_intro zenon_H28a. zenon_intro zenon_He6. % 1.14/1.30 exact (zenon_He6 zenon_H36). % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H284); [ zenon_intro zenon_H28c | zenon_intro zenon_H28b ]. % 1.14/1.30 cut (((op (e0) (e0)) = (e0)) = ((op (op (e0) (e0)) (op (e0) (e0))) = (e0))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H28c. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H9. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e0) (e0)) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H28d]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [ zenon_intro zenon_H28e | zenon_intro zenon_H28f ]. % 1.14/1.30 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0)))) = ((op (e0) (e0)) = (op (op (e0) (e0)) (op (e0) (e0))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H28d. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H28e. % 1.14/1.30 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (op (e0) (e0)) (op (e0) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H28f]. % 1.14/1.30 cut (((op (op (e0) (e0)) (op (e0) (e0))) = (op (e0) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H290]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e0) (e0)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 1.14/1.30 cut (((op (e0) (e0)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3e]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H3e zenon_H9). % 1.14/1.30 exact (zenon_H3e zenon_H9). % 1.14/1.30 apply zenon_H28f. apply refl_equal. % 1.14/1.30 apply zenon_H28f. apply refl_equal. % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H28b); [ zenon_intro zenon_H292 | zenon_intro zenon_H291 ]. % 1.14/1.30 cut (((op (e2) (e3)) = (e0)) = ((op (op (e1) (e0)) (op (e0) (e1))) = (e0))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H292. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H23. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e2) (e3)) = (op (op (e1) (e0)) (op (e0) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H293]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e1) (e0)) (op (e0) (e1))) = (op (op (e1) (e0)) (op (e0) (e1))))); [ zenon_intro zenon_H294 | zenon_intro zenon_H295 ]. % 1.14/1.30 cut (((op (op (e1) (e0)) (op (e0) (e1))) = (op (op (e1) (e0)) (op (e0) (e1)))) = ((op (e2) (e3)) = (op (op (e1) (e0)) (op (e0) (e1))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H293. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H294. % 1.14/1.30 cut (((op (op (e1) (e0)) (op (e0) (e1))) = (op (op (e1) (e0)) (op (e0) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H295]. % 1.14/1.30 cut (((op (op (e1) (e0)) (op (e0) (e1))) = (op (e2) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H296]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e0) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 1.14/1.30 cut (((op (e1) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H61 zenon_H13). % 1.14/1.30 exact (zenon_H45 zenon_Hb). % 1.14/1.30 apply zenon_H295. apply refl_equal. % 1.14/1.30 apply zenon_H295. apply refl_equal. % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H291); [ zenon_intro zenon_H298 | zenon_intro zenon_H297 ]. % 1.14/1.30 cut (((op (e1) (e4)) = (e0)) = ((op (op (e2) (e0)) (op (e0) (e2))) = (e0))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H298. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H1b. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e1) (e4)) = (op (op (e2) (e0)) (op (e0) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H299]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e0)) (op (e0) (e2))) = (op (op (e2) (e0)) (op (e0) (e2))))); [ zenon_intro zenon_H29a | zenon_intro zenon_H29b ]. % 1.14/1.30 cut (((op (op (e2) (e0)) (op (e0) (e2))) = (op (op (e2) (e0)) (op (e0) (e2)))) = ((op (e1) (e4)) = (op (op (e2) (e0)) (op (e0) (e2))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H299. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H29a. % 1.14/1.30 cut (((op (op (e2) (e0)) (op (e0) (e2))) = (op (op (e2) (e0)) (op (e0) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H29b]. % 1.14/1.30 cut (((op (op (e2) (e0)) (op (e0) (e2))) = (op (e1) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H29c]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e0) (e2)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 1.14/1.30 cut (((op (e2) (e0)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H84]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H84 zenon_H1d). % 1.14/1.30 exact (zenon_H4c zenon_Hd). % 1.14/1.30 apply zenon_H29b. apply refl_equal. % 1.14/1.30 apply zenon_H29b. apply refl_equal. % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H297); [ zenon_intro zenon_H29e | zenon_intro zenon_H29d ]. % 1.14/1.30 cut (((op (e4) (e2)) = (e0)) = ((op (op (e3) (e0)) (op (e0) (e3))) = (e0))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H29e. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H35. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e4) (e2)) = (op (op (e3) (e0)) (op (e0) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H29f]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e0)) (op (e0) (e3))) = (op (op (e3) (e0)) (op (e0) (e3))))); [ zenon_intro zenon_H2a0 | zenon_intro zenon_H2a1 ]. % 1.14/1.30 cut (((op (op (e3) (e0)) (op (e0) (e3))) = (op (op (e3) (e0)) (op (e0) (e3)))) = ((op (e4) (e2)) = (op (op (e3) (e0)) (op (e0) (e3))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H29f. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2a0. % 1.14/1.30 cut (((op (op (e3) (e0)) (op (e0) (e3))) = (op (op (e3) (e0)) (op (e0) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2a1]. % 1.14/1.30 cut (((op (op (e3) (e0)) (op (e0) (e3))) = (op (e4) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H2a2]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e0) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 1.14/1.30 cut (((op (e3) (e0)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Ha7 zenon_H27). % 1.14/1.30 exact (zenon_H53 zenon_Hf). % 1.14/1.30 apply zenon_H2a1. apply refl_equal. % 1.14/1.30 apply zenon_H2a1. apply refl_equal. % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H29d); [ zenon_intro zenon_H2a4 | zenon_intro zenon_H2a3 ]. % 1.14/1.30 cut (((op (e3) (e1)) = (e0)) = ((op (op (e4) (e0)) (op (e0) (e4))) = (e0))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2a4. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H29. % 1.14/1.30 cut (((e0) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H3]. % 1.14/1.30 cut (((op (e3) (e1)) = (op (op (e4) (e0)) (op (e0) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2a5]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e0)) (op (e0) (e4))) = (op (op (e4) (e0)) (op (e0) (e4))))); [ zenon_intro zenon_H2a6 | zenon_intro zenon_H2a7 ]. % 1.14/1.30 cut (((op (op (e4) (e0)) (op (e0) (e4))) = (op (op (e4) (e0)) (op (e0) (e4)))) = ((op (e3) (e1)) = (op (op (e4) (e0)) (op (e0) (e4))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2a5. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2a6. % 1.14/1.30 cut (((op (op (e4) (e0)) (op (e0) (e4))) = (op (op (e4) (e0)) (op (e0) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2a7]. % 1.14/1.30 cut (((op (op (e4) (e0)) (op (e0) (e4))) = (op (e3) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H2a8]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e0) (e4)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 1.14/1.30 cut (((op (e4) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hca zenon_H31). % 1.14/1.30 exact (zenon_H5a zenon_H11). % 1.14/1.30 apply zenon_H2a7. apply refl_equal. % 1.14/1.30 apply zenon_H2a7. apply refl_equal. % 1.14/1.30 apply zenon_H3. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2a3); [ zenon_intro zenon_H2aa | zenon_intro zenon_H2a9 ]. % 1.14/1.30 cut (((op (e3) (e2)) = (e1)) = ((op (op (e0) (e1)) (op (e1) (e0))) = (e1))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2aa. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2b. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e3) (e2)) = (op (op (e0) (e1)) (op (e1) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H2ab]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e0) (e1)) (op (e1) (e0))) = (op (op (e0) (e1)) (op (e1) (e0))))); [ zenon_intro zenon_H2ac | zenon_intro zenon_H2ad ]. % 1.14/1.30 cut (((op (op (e0) (e1)) (op (e1) (e0))) = (op (op (e0) (e1)) (op (e1) (e0)))) = ((op (e3) (e2)) = (op (op (e0) (e1)) (op (e1) (e0))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2ab. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2ac. % 1.14/1.30 cut (((op (op (e0) (e1)) (op (e1) (e0))) = (op (op (e0) (e1)) (op (e1) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H2ad]. % 1.14/1.30 cut (((op (op (e0) (e1)) (op (e1) (e0))) = (op (e3) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H2ae]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e1) (e0)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H61]. % 1.14/1.30 cut (((op (e0) (e1)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H45]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H45 zenon_Hb). % 1.14/1.30 exact (zenon_H61 zenon_H13). % 1.14/1.30 apply zenon_H2ad. apply refl_equal. % 1.14/1.30 apply zenon_H2ad. apply refl_equal. % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2a9); [ zenon_intro zenon_H2b0 | zenon_intro zenon_H2af ]. % 1.14/1.30 cut (((op (e1) (e1)) = (e1)) = ((op (op (e1) (e1)) (op (e1) (e1))) = (e1))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2b0. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H15. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e1) (e1)) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H2b1]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [ zenon_intro zenon_H2b2 | zenon_intro zenon_H2b3 ]. % 1.14/1.30 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1)))) = ((op (e1) (e1)) = (op (op (e1) (e1)) (op (e1) (e1))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2b1. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2b2. % 1.14/1.30 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (op (e1) (e1)) (op (e1) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H2b3]. % 1.14/1.30 cut (((op (op (e1) (e1)) (op (e1) (e1))) = (op (e1) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H2b4]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e1) (e1)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 1.14/1.30 cut (((op (e1) (e1)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H68]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H68 zenon_H15). % 1.14/1.30 exact (zenon_H68 zenon_H15). % 1.14/1.30 apply zenon_H2b3. apply refl_equal. % 1.14/1.30 apply zenon_H2b3. apply refl_equal. % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2af); [ zenon_intro zenon_H2b6 | zenon_intro zenon_H2b5 ]. % 1.14/1.30 cut (((op (e4) (e3)) = (e1)) = ((op (op (e2) (e1)) (op (e1) (e2))) = (e1))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2b6. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H37. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e4) (e3)) = (op (op (e2) (e1)) (op (e1) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H2b7]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e1)) (op (e1) (e2))) = (op (op (e2) (e1)) (op (e1) (e2))))); [ zenon_intro zenon_H2b8 | zenon_intro zenon_H2b9 ]. % 1.14/1.30 cut (((op (op (e2) (e1)) (op (e1) (e2))) = (op (op (e2) (e1)) (op (e1) (e2)))) = ((op (e4) (e3)) = (op (op (e2) (e1)) (op (e1) (e2))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2b7. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2b8. % 1.14/1.30 cut (((op (op (e2) (e1)) (op (e1) (e2))) = (op (op (e2) (e1)) (op (e1) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H2b9]. % 1.14/1.30 cut (((op (op (e2) (e1)) (op (e1) (e2))) = (op (e4) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H2ba]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e1) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6f]. % 1.14/1.30 cut (((op (e2) (e1)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H8b zenon_H1f). % 1.14/1.30 exact (zenon_H6f zenon_H17). % 1.14/1.30 apply zenon_H2b9. apply refl_equal. % 1.14/1.30 apply zenon_H2b9. apply refl_equal. % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2b5); [ zenon_intro zenon_H2bc | zenon_intro zenon_H2bb ]. % 1.14/1.30 cut (((op (e0) (e4)) = (e1)) = ((op (op (e3) (e1)) (op (e1) (e3))) = (e1))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2bc. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H11. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e0) (e4)) = (op (op (e3) (e1)) (op (e1) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2bd]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e1)) (op (e1) (e3))) = (op (op (e3) (e1)) (op (e1) (e3))))); [ zenon_intro zenon_H2be | zenon_intro zenon_H2bf ]. % 1.14/1.30 cut (((op (op (e3) (e1)) (op (e1) (e3))) = (op (op (e3) (e1)) (op (e1) (e3)))) = ((op (e0) (e4)) = (op (op (e3) (e1)) (op (e1) (e3))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2bd. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2be. % 1.14/1.30 cut (((op (op (e3) (e1)) (op (e1) (e3))) = (op (op (e3) (e1)) (op (e1) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2bf]. % 1.14/1.30 cut (((op (op (e3) (e1)) (op (e1) (e3))) = (op (e0) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H2c0]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e1) (e3)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H76]. % 1.14/1.30 cut (((op (e3) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hae zenon_H29). % 1.14/1.30 exact (zenon_H76 zenon_H19). % 1.14/1.30 apply zenon_H2bf. apply refl_equal. % 1.14/1.30 apply zenon_H2bf. apply refl_equal. % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2bb); [ zenon_intro zenon_H2c2 | zenon_intro zenon_H2c1 ]. % 1.14/1.30 cut (((op (e2) (e0)) = (e1)) = ((op (op (e4) (e1)) (op (e1) (e4))) = (e1))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2c2. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H1d. % 1.14/1.30 cut (((e1) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H4]. % 1.14/1.30 cut (((op (e2) (e0)) = (op (op (e4) (e1)) (op (e1) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2c3]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e1)) (op (e1) (e4))) = (op (op (e4) (e1)) (op (e1) (e4))))); [ zenon_intro zenon_H2c4 | zenon_intro zenon_H2c5 ]. % 1.14/1.30 cut (((op (op (e4) (e1)) (op (e1) (e4))) = (op (op (e4) (e1)) (op (e1) (e4)))) = ((op (e2) (e0)) = (op (op (e4) (e1)) (op (e1) (e4))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2c3. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2c4. % 1.14/1.30 cut (((op (op (e4) (e1)) (op (e1) (e4))) = (op (op (e4) (e1)) (op (e1) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2c5]. % 1.14/1.30 cut (((op (op (e4) (e1)) (op (e1) (e4))) = (op (e2) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H2c6]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e1) (e4)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 1.14/1.30 cut (((op (e4) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hd1 zenon_H33). % 1.14/1.30 exact (zenon_H7d zenon_H1b). % 1.14/1.30 apply zenon_H2c5. apply refl_equal. % 1.14/1.30 apply zenon_H2c5. apply refl_equal. % 1.14/1.30 apply zenon_H4. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2c1); [ zenon_intro zenon_H2c8 | zenon_intro zenon_H2c7 ]. % 1.14/1.30 cut (((op (e4) (e1)) = (e2)) = ((op (op (e0) (e2)) (op (e2) (e0))) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2c8. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H33. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e4) (e1)) = (op (op (e0) (e2)) (op (e2) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H2c9]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e0) (e2)) (op (e2) (e0))) = (op (op (e0) (e2)) (op (e2) (e0))))); [ zenon_intro zenon_H2ca | zenon_intro zenon_H2cb ]. % 1.14/1.30 cut (((op (op (e0) (e2)) (op (e2) (e0))) = (op (op (e0) (e2)) (op (e2) (e0)))) = ((op (e4) (e1)) = (op (op (e0) (e2)) (op (e2) (e0))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2c9. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2ca. % 1.14/1.30 cut (((op (op (e0) (e2)) (op (e2) (e0))) = (op (op (e0) (e2)) (op (e2) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H2cb]. % 1.14/1.30 cut (((op (op (e0) (e2)) (op (e2) (e0))) = (op (e4) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H2cc]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e2) (e0)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H84]. % 1.14/1.30 cut (((op (e0) (e2)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H4c]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H4c zenon_Hd). % 1.14/1.30 exact (zenon_H84 zenon_H1d). % 1.14/1.30 apply zenon_H2cb. apply refl_equal. % 1.14/1.30 apply zenon_H2cb. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2c7); [ zenon_intro zenon_H2ce | zenon_intro zenon_H2cd ]. % 1.14/1.30 cut (((op (e3) (e4)) = (e2)) = ((op (op (e1) (e2)) (op (e2) (e1))) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2ce. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2f. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e3) (e4)) = (op (op (e1) (e2)) (op (e2) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H2cf]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e1) (e2)) (op (e2) (e1))) = (op (op (e1) (e2)) (op (e2) (e1))))); [ zenon_intro zenon_H2d0 | zenon_intro zenon_H2d1 ]. % 1.14/1.30 cut (((op (op (e1) (e2)) (op (e2) (e1))) = (op (op (e1) (e2)) (op (e2) (e1)))) = ((op (e3) (e4)) = (op (op (e1) (e2)) (op (e2) (e1))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2cf. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2d0. % 1.14/1.30 cut (((op (op (e1) (e2)) (op (e2) (e1))) = (op (op (e1) (e2)) (op (e2) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H2d1]. % 1.14/1.30 cut (((op (op (e1) (e2)) (op (e2) (e1))) = (op (e3) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H2d2]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e2) (e1)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 1.14/1.30 cut (((op (e1) (e2)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6f]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H6f zenon_H17). % 1.14/1.30 exact (zenon_H8b zenon_H1f). % 1.14/1.30 apply zenon_H2d1. apply refl_equal. % 1.14/1.30 apply zenon_H2d1. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2cd); [ zenon_intro zenon_H2d4 | zenon_intro zenon_H2d3 ]. % 1.14/1.30 cut (((op (e2) (e2)) = (e2)) = ((op (op (e2) (e2)) (op (e2) (e2))) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2d4. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H21. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e2) (e2)) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H2d5]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [ zenon_intro zenon_H2d6 | zenon_intro zenon_H2d7 ]. % 1.14/1.30 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2)))) = ((op (e2) (e2)) = (op (op (e2) (e2)) (op (e2) (e2))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2d5. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2d6. % 1.14/1.30 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (op (e2) (e2)) (op (e2) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H2d7]. % 1.14/1.30 cut (((op (op (e2) (e2)) (op (e2) (e2))) = (op (e2) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H2d8]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e2) (e2)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H92]. % 1.14/1.30 cut (((op (e2) (e2)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H92]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H92 zenon_H21). % 1.14/1.30 exact (zenon_H92 zenon_H21). % 1.14/1.30 apply zenon_H2d7. apply refl_equal. % 1.14/1.30 apply zenon_H2d7. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2d3); [ zenon_intro zenon_H2da | zenon_intro zenon_H2d9 ]. % 1.14/1.30 cut (((op (e1) (e0)) = (e2)) = ((op (op (e3) (e2)) (op (e2) (e3))) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2da. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H13. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e1) (e0)) = (op (op (e3) (e2)) (op (e2) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2db]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e2)) (op (e2) (e3))) = (op (op (e3) (e2)) (op (e2) (e3))))); [ zenon_intro zenon_H2dc | zenon_intro zenon_H2dd ]. % 1.14/1.30 cut (((op (op (e3) (e2)) (op (e2) (e3))) = (op (op (e3) (e2)) (op (e2) (e3)))) = ((op (e1) (e0)) = (op (op (e3) (e2)) (op (e2) (e3))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2db. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2dc. % 1.14/1.30 cut (((op (op (e3) (e2)) (op (e2) (e3))) = (op (op (e3) (e2)) (op (e2) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2dd]. % 1.14/1.30 cut (((op (op (e3) (e2)) (op (e2) (e3))) = (op (e1) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H2de]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e2) (e3)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 1.14/1.30 cut (((op (e3) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hb5 zenon_H2b). % 1.14/1.30 exact (zenon_H99 zenon_H23). % 1.14/1.30 apply zenon_H2dd. apply refl_equal. % 1.14/1.30 apply zenon_H2dd. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2d9); [ zenon_intro zenon_H2e0 | zenon_intro zenon_H2df ]. % 1.14/1.30 cut (((op (e0) (e3)) = (e2)) = ((op (op (e4) (e2)) (op (e2) (e4))) = (e2))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2e0. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hf. % 1.14/1.30 cut (((e2) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H5]. % 1.14/1.30 cut (((op (e0) (e3)) = (op (op (e4) (e2)) (op (e2) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2e1]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e2)) (op (e2) (e4))) = (op (op (e4) (e2)) (op (e2) (e4))))); [ zenon_intro zenon_H2e2 | zenon_intro zenon_H2e3 ]. % 1.14/1.30 cut (((op (op (e4) (e2)) (op (e2) (e4))) = (op (op (e4) (e2)) (op (e2) (e4)))) = ((op (e0) (e3)) = (op (op (e4) (e2)) (op (e2) (e4))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2e1. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2e2. % 1.14/1.30 cut (((op (op (e4) (e2)) (op (e2) (e4))) = (op (op (e4) (e2)) (op (e2) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2e3]. % 1.14/1.30 cut (((op (op (e4) (e2)) (op (e2) (e4))) = (op (e0) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H2e4]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e2) (e4)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 1.14/1.30 cut (((op (e4) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hd8 zenon_H35). % 1.14/1.30 exact (zenon_Ha0 zenon_H25). % 1.14/1.30 apply zenon_H2e3. apply refl_equal. % 1.14/1.30 apply zenon_H2e3. apply refl_equal. % 1.14/1.30 apply zenon_H5. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2df); [ zenon_intro zenon_H2e6 | zenon_intro zenon_H2e5 ]. % 1.14/1.30 cut (((op (e2) (e4)) = (e3)) = ((op (op (e0) (e3)) (op (e3) (e0))) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2e6. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H25. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e2) (e4)) = (op (op (e0) (e3)) (op (e3) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H2e7]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e0) (e3)) (op (e3) (e0))) = (op (op (e0) (e3)) (op (e3) (e0))))); [ zenon_intro zenon_H2e8 | zenon_intro zenon_H2e9 ]. % 1.14/1.30 cut (((op (op (e0) (e3)) (op (e3) (e0))) = (op (op (e0) (e3)) (op (e3) (e0)))) = ((op (e2) (e4)) = (op (op (e0) (e3)) (op (e3) (e0))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2e7. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2e8. % 1.14/1.30 cut (((op (op (e0) (e3)) (op (e3) (e0))) = (op (op (e0) (e3)) (op (e3) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H2e9]. % 1.14/1.30 cut (((op (op (e0) (e3)) (op (e3) (e0))) = (op (e2) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H2ea]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e3) (e0)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_Ha7]. % 1.14/1.30 cut (((op (e0) (e3)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_H53]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H53 zenon_Hf). % 1.14/1.30 exact (zenon_Ha7 zenon_H27). % 1.14/1.30 apply zenon_H2e9. apply refl_equal. % 1.14/1.30 apply zenon_H2e9. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2e5); [ zenon_intro zenon_H2ec | zenon_intro zenon_H2eb ]. % 1.14/1.30 cut (((op (e4) (e0)) = (e3)) = ((op (op (e1) (e3)) (op (e3) (e1))) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2ec. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H31. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e4) (e0)) = (op (op (e1) (e3)) (op (e3) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H2ed]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e1) (e3)) (op (e3) (e1))) = (op (op (e1) (e3)) (op (e3) (e1))))); [ zenon_intro zenon_H2ee | zenon_intro zenon_H2ef ]. % 1.14/1.30 cut (((op (op (e1) (e3)) (op (e3) (e1))) = (op (op (e1) (e3)) (op (e3) (e1)))) = ((op (e4) (e0)) = (op (op (e1) (e3)) (op (e3) (e1))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2ed. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2ee. % 1.14/1.30 cut (((op (op (e1) (e3)) (op (e3) (e1))) = (op (op (e1) (e3)) (op (e3) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H2ef]. % 1.14/1.30 cut (((op (op (e1) (e3)) (op (e3) (e1))) = (op (e4) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H2f0]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e3) (e1)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hae]. % 1.14/1.30 cut (((op (e1) (e3)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H76]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H76 zenon_H19). % 1.14/1.30 exact (zenon_Hae zenon_H29). % 1.14/1.30 apply zenon_H2ef. apply refl_equal. % 1.14/1.30 apply zenon_H2ef. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2eb); [ zenon_intro zenon_H2f2 | zenon_intro zenon_H2f1 ]. % 1.14/1.30 cut (((op (e0) (e1)) = (e3)) = ((op (op (e2) (e3)) (op (e3) (e2))) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2f2. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hb. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e0) (e1)) = (op (op (e2) (e3)) (op (e3) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H2f3]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e3)) (op (e3) (e2))) = (op (op (e2) (e3)) (op (e3) (e2))))); [ zenon_intro zenon_H2f4 | zenon_intro zenon_H2f5 ]. % 1.14/1.30 cut (((op (op (e2) (e3)) (op (e3) (e2))) = (op (op (e2) (e3)) (op (e3) (e2)))) = ((op (e0) (e1)) = (op (op (e2) (e3)) (op (e3) (e2))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2f3. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2f4. % 1.14/1.30 cut (((op (op (e2) (e3)) (op (e3) (e2))) = (op (op (e2) (e3)) (op (e3) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H2f5]. % 1.14/1.30 cut (((op (op (e2) (e3)) (op (e3) (e2))) = (op (e0) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H2f6]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e3) (e2)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hb5]. % 1.14/1.30 cut (((op (e2) (e3)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H99]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H99 zenon_H23). % 1.14/1.30 exact (zenon_Hb5 zenon_H2b). % 1.14/1.30 apply zenon_H2f5. apply refl_equal. % 1.14/1.30 apply zenon_H2f5. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2f1); [ zenon_intro zenon_H2f8 | zenon_intro zenon_H2f7 ]. % 1.14/1.30 cut (((op (e3) (e3)) = (e3)) = ((op (op (e3) (e3)) (op (e3) (e3))) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2f8. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2d. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e3) (e3)) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2f9]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [ zenon_intro zenon_H2fa | zenon_intro zenon_H2fb ]. % 1.14/1.30 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3)))) = ((op (e3) (e3)) = (op (op (e3) (e3)) (op (e3) (e3))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2f9. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H2fa. % 1.14/1.30 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (op (e3) (e3)) (op (e3) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H2fb]. % 1.14/1.30 cut (((op (op (e3) (e3)) (op (e3) (e3))) = (op (e3) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H2fc]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e3) (e3)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 1.14/1.30 cut (((op (e3) (e3)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hbc]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hbc zenon_H2d). % 1.14/1.30 exact (zenon_Hbc zenon_H2d). % 1.14/1.30 apply zenon_H2fb. apply refl_equal. % 1.14/1.30 apply zenon_H2fb. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2f7); [ zenon_intro zenon_H2fe | zenon_intro zenon_H2fd ]. % 1.14/1.30 cut (((op (e1) (e2)) = (e3)) = ((op (op (e4) (e3)) (op (e3) (e4))) = (e3))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2fe. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H17. % 1.14/1.30 cut (((e3) = (e3))); [idtac | apply NNPP; zenon_intro zenon_H6]. % 1.14/1.30 cut (((op (e1) (e2)) = (op (op (e4) (e3)) (op (e3) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H2ff]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e3)) (op (e3) (e4))) = (op (op (e4) (e3)) (op (e3) (e4))))); [ zenon_intro zenon_H300 | zenon_intro zenon_H301 ]. % 1.14/1.30 cut (((op (op (e4) (e3)) (op (e3) (e4))) = (op (op (e4) (e3)) (op (e3) (e4)))) = ((op (e1) (e2)) = (op (op (e4) (e3)) (op (e3) (e4))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H2ff. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H300. % 1.14/1.30 cut (((op (op (e4) (e3)) (op (e3) (e4))) = (op (op (e4) (e3)) (op (e3) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H301]. % 1.14/1.30 cut (((op (op (e4) (e3)) (op (e3) (e4))) = (op (e1) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H302]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e3) (e4)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 1.14/1.30 cut (((op (e4) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hdf]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hdf zenon_H37). % 1.14/1.30 exact (zenon_Hc3 zenon_H2f). % 1.14/1.30 apply zenon_H301. apply refl_equal. % 1.14/1.30 apply zenon_H301. apply refl_equal. % 1.14/1.30 apply zenon_H6. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H2fd); [ zenon_intro zenon_H304 | zenon_intro zenon_H303 ]. % 1.14/1.30 cut (((op (e1) (e3)) = (e4)) = ((op (op (e0) (e4)) (op (e4) (e0))) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H304. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H19. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e1) (e3)) = (op (op (e0) (e4)) (op (e4) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H305]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e0) (e4)) (op (e4) (e0))) = (op (op (e0) (e4)) (op (e4) (e0))))); [ zenon_intro zenon_H306 | zenon_intro zenon_H307 ]. % 1.14/1.30 cut (((op (op (e0) (e4)) (op (e4) (e0))) = (op (op (e0) (e4)) (op (e4) (e0)))) = ((op (e1) (e3)) = (op (op (e0) (e4)) (op (e4) (e0))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H305. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H306. % 1.14/1.30 cut (((op (op (e0) (e4)) (op (e4) (e0))) = (op (op (e0) (e4)) (op (e4) (e0))))); [idtac | apply NNPP; zenon_intro zenon_H307]. % 1.14/1.30 cut (((op (op (e0) (e4)) (op (e4) (e0))) = (op (e1) (e3)))); [idtac | apply NNPP; zenon_intro zenon_H308]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e4) (e0)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Hca]. % 1.14/1.30 cut (((op (e0) (e4)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_H5a]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H5a zenon_H11). % 1.14/1.30 exact (zenon_Hca zenon_H31). % 1.14/1.30 apply zenon_H307. apply refl_equal. % 1.14/1.30 apply zenon_H307. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H303); [ zenon_intro zenon_H30a | zenon_intro zenon_H309 ]. % 1.14/1.30 cut (((op (e0) (e2)) = (e4)) = ((op (op (e1) (e4)) (op (e4) (e1))) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H30a. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_Hd. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e0) (e2)) = (op (op (e1) (e4)) (op (e4) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H30b]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e1) (e4)) (op (e4) (e1))) = (op (op (e1) (e4)) (op (e4) (e1))))); [ zenon_intro zenon_H30c | zenon_intro zenon_H30d ]. % 1.14/1.30 cut (((op (op (e1) (e4)) (op (e4) (e1))) = (op (op (e1) (e4)) (op (e4) (e1)))) = ((op (e0) (e2)) = (op (op (e1) (e4)) (op (e4) (e1))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H30b. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H30c. % 1.14/1.30 cut (((op (op (e1) (e4)) (op (e4) (e1))) = (op (op (e1) (e4)) (op (e4) (e1))))); [idtac | apply NNPP; zenon_intro zenon_H30d]. % 1.14/1.30 cut (((op (op (e1) (e4)) (op (e4) (e1))) = (op (e0) (e2)))); [idtac | apply NNPP; zenon_intro zenon_H30e]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e4) (e1)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_Hd1]. % 1.14/1.30 cut (((op (e1) (e4)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_H7d]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_H7d zenon_H1b). % 1.14/1.30 exact (zenon_Hd1 zenon_H33). % 1.14/1.30 apply zenon_H30d. apply refl_equal. % 1.14/1.30 apply zenon_H30d. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H309); [ zenon_intro zenon_H310 | zenon_intro zenon_H30f ]. % 1.14/1.30 cut (((op (e3) (e0)) = (e4)) = ((op (op (e2) (e4)) (op (e4) (e2))) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H310. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H27. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e3) (e0)) = (op (op (e2) (e4)) (op (e4) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H311]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e2) (e4)) (op (e4) (e2))) = (op (op (e2) (e4)) (op (e4) (e2))))); [ zenon_intro zenon_H312 | zenon_intro zenon_H313 ]. % 1.14/1.30 cut (((op (op (e2) (e4)) (op (e4) (e2))) = (op (op (e2) (e4)) (op (e4) (e2)))) = ((op (e3) (e0)) = (op (op (e2) (e4)) (op (e4) (e2))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H311. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H312. % 1.14/1.30 cut (((op (op (e2) (e4)) (op (e4) (e2))) = (op (op (e2) (e4)) (op (e4) (e2))))); [idtac | apply NNPP; zenon_intro zenon_H313]. % 1.14/1.30 cut (((op (op (e2) (e4)) (op (e4) (e2))) = (op (e3) (e0)))); [idtac | apply NNPP; zenon_intro zenon_H314]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e4) (e2)) = (e0))); [idtac | apply NNPP; zenon_intro zenon_Hd8]. % 1.14/1.30 cut (((op (e2) (e4)) = (e3))); [idtac | apply NNPP; zenon_intro zenon_Ha0]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Ha0 zenon_H25). % 1.14/1.30 exact (zenon_Hd8 zenon_H35). % 1.14/1.30 apply zenon_H313. apply refl_equal. % 1.14/1.30 apply zenon_H313. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 apply (zenon_notand_s _ _ zenon_H30f); [ zenon_intro zenon_H316 | zenon_intro zenon_H315 ]. % 1.14/1.30 cut (((op (e2) (e1)) = (e4)) = ((op (op (e3) (e4)) (op (e4) (e3))) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H316. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H1f. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e2) (e1)) = (op (op (e3) (e4)) (op (e4) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H317]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e3) (e4)) (op (e4) (e3))) = (op (op (e3) (e4)) (op (e4) (e3))))); [ zenon_intro zenon_H318 | zenon_intro zenon_H319 ]. % 1.14/1.30 cut (((op (op (e3) (e4)) (op (e4) (e3))) = (op (op (e3) (e4)) (op (e4) (e3)))) = ((op (e2) (e1)) = (op (op (e3) (e4)) (op (e4) (e3))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H317. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H318. % 1.14/1.30 cut (((op (op (e3) (e4)) (op (e4) (e3))) = (op (op (e3) (e4)) (op (e4) (e3))))); [idtac | apply NNPP; zenon_intro zenon_H319]. % 1.14/1.30 cut (((op (op (e3) (e4)) (op (e4) (e3))) = (op (e2) (e1)))); [idtac | apply NNPP; zenon_intro zenon_H31a]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e4) (e3)) = (e1))); [idtac | apply NNPP; zenon_intro zenon_Hdf]. % 1.14/1.30 cut (((op (e3) (e4)) = (e2))); [idtac | apply NNPP; zenon_intro zenon_Hc3]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_Hc3 zenon_H2f). % 1.14/1.30 exact (zenon_Hdf zenon_H37). % 1.14/1.30 apply zenon_H319. apply refl_equal. % 1.14/1.30 apply zenon_H319. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 cut (((op (e4) (e4)) = (e4)) = ((op (op (e4) (e4)) (op (e4) (e4))) = (e4))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H315. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H36. % 1.14/1.30 cut (((e4) = (e4))); [idtac | apply NNPP; zenon_intro zenon_H7]. % 1.14/1.30 cut (((op (e4) (e4)) = (op (op (e4) (e4)) (op (e4) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H31b]. % 1.14/1.30 congruence. % 1.14/1.30 elim (classic ((op (op (e4) (e4)) (op (e4) (e4))) = (op (op (e4) (e4)) (op (e4) (e4))))); [ zenon_intro zenon_H31c | zenon_intro zenon_H31d ]. % 1.14/1.30 cut (((op (op (e4) (e4)) (op (e4) (e4))) = (op (op (e4) (e4)) (op (e4) (e4)))) = ((op (e4) (e4)) = (op (op (e4) (e4)) (op (e4) (e4))))). % 1.14/1.30 intro zenon_D_pnotp. % 1.14/1.30 apply zenon_H31b. % 1.14/1.30 rewrite <- zenon_D_pnotp. % 1.14/1.30 exact zenon_H31c. % 1.14/1.30 cut (((op (op (e4) (e4)) (op (e4) (e4))) = (op (op (e4) (e4)) (op (e4) (e4))))); [idtac | apply NNPP; zenon_intro zenon_H31d]. % 1.14/1.30 cut (((op (op (e4) (e4)) (op (e4) (e4))) = (op (e4) (e4)))); [idtac | apply NNPP; zenon_intro zenon_H31e]. % 1.14/1.30 congruence. % 1.14/1.30 cut (((op (e4) (e4)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 1.14/1.30 cut (((op (e4) (e4)) = (e4))); [idtac | apply NNPP; zenon_intro zenon_He6]. % 1.14/1.30 congruence. % 1.14/1.30 exact (zenon_He6 zenon_H36). % 1.14/1.30 exact (zenon_He6 zenon_H36). % 1.14/1.30 apply zenon_H31d. apply refl_equal. % 1.14/1.30 apply zenon_H31d. apply refl_equal. % 1.14/1.30 apply zenon_H7. apply refl_equal. % 1.14/1.30 Qed. % 1.14/1.30 % SZS output end Proof % 1.14/1.30 (* END-PROOF *) % 1.14/1.30 nodes searched: 6033 % 1.14/1.30 max branch formulas: 145 % 1.14/1.30 proof nodes created: 332 % 1.14/1.30 formulas created: 20021 % 1.14/1.30 %------------------------------------------------------------------------------