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