%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : ALG072+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:06:59 AM UTC 2026
% Result : Theorem 1.21s 0.41s
% Output : Proof 2.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG072+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.17 % Computer : n013.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 19:24:06 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.21/0.41 Command-line arguments: --flatten --complete-subsets
% 1.21/0.41
% 1.21/0.41 % SZS status Theorem
% 1.21/0.41
% 1.21/0.51 % SZS output start Proof
% 1.21/0.51 Axiom 1 (ax2): unit1 = v3.
% 1.21/0.51 Axiom 2 (ax4): unit2 = v2.
% 1.21/0.51 Axiom 3 (ax4_1): sorti2(v2) = true.
% 1.21/0.51 Axiom 4 (ax2_1): sorti1(v3) = true.
% 1.21/0.51 Axiom 5 (ax7): sorti1(u) = true.
% 1.21/0.51 Axiom 6 (ifeq_axiom): ifeq3(X, X, Y, Z) = Y.
% 1.21/0.51 Axiom 7 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 1.21/0.51 Axiom 8 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 1.21/0.51 Axiom 9 (ax8_2): ifeq(sorti2(X), true, sorti2(v(X)), true) = true.
% 1.21/0.51 Axiom 10 (ax8_3): ifeq(sorti2(X), true, sorti2(w(X)), true) = true.
% 1.21/0.51 Axiom 11 (co1_3): ifeq(sorti2(X), true, sorti1(j(X)), true) = true.
% 1.21/0.51 Axiom 12 (co1): ifeq(sorti1(X), true, sorti2(h(X)), true) = true.
% 1.21/0.51 Axiom 13 (co1_5): ifeq2(sorti2(X), true, h(j(X)), X) = X.
% 1.21/0.51 Axiom 14 (ax4_2): ifeq2(sorti2(X), true, op2(X, unit2), X) = X.
% 1.21/0.51 Axiom 15 (co1_2): ifeq2(sorti1(X), true, j(h(X)), X) = X.
% 1.21/0.51 Axiom 16 (ax2_2): ifeq2(sorti1(X), true, op1(X, unit1), X) = X.
% 1.21/0.51 Axiom 17 (ax2_3): ifeq2(sorti1(X), true, op1(unit1, X), X) = X.
% 1.21/0.51 Axiom 18 (ax8_1): ifeq2(sorti2(X), true, op2(v(X), w(X)), X) = X.
% 1.21/0.51 Axiom 19 (ax8): ifeq2(sorti2(X), true, ifeq3(op2(v(X), X), w(X), X, unit2), unit2) = unit2.
% 1.21/0.51 Axiom 20 (co1_4): ifeq2(sorti2(X), true, ifeq2(sorti2(Y), true, op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X))) = j(op2(Y, X)).
% 1.21/0.51 Axiom 21 (ax7_2): ifeq2(sorti1(X), true, ifeq2(sorti1(Y), true, ifeq3(op1(Y, X), u, op1(Y, u), X), X), X) = X.
% 1.21/0.51 Axiom 22 (co1_1): ifeq2(sorti1(X), true, ifeq2(sorti1(Y), true, op2(h(Y), h(X)), h(op1(Y, X))), h(op1(Y, X))) = h(op1(Y, X)).
% 1.21/0.51
% 1.21/0.51 Lemma 23: sorti1(v3) = sorti2(unit2).
% 1.21/0.51 Proof:
% 1.21/0.51 sorti1(v3)
% 1.21/0.51 = { by axiom 4 (ax2_1) }
% 1.21/0.51 true
% 1.21/0.51 = { by axiom 3 (ax4_1) R->L }
% 1.21/0.51 sorti2(v2)
% 1.21/0.51 = { by axiom 2 (ax4) R->L }
% 1.21/0.51 sorti2(unit2)
% 1.21/0.51
% 1.21/0.51 Lemma 24: sorti1(u) = sorti1(unit1).
% 1.21/0.51 Proof:
% 1.21/0.51 sorti1(u)
% 1.21/0.51 = { by axiom 5 (ax7) }
% 1.21/0.51 true
% 1.21/0.51 = { by axiom 3 (ax4_1) R->L }
% 1.21/0.51 sorti2(v2)
% 1.21/0.51 = { by axiom 2 (ax4) R->L }
% 1.21/0.51 sorti2(unit2)
% 1.21/0.51 = { by lemma 23 R->L }
% 1.21/0.51 sorti1(v3)
% 1.21/0.51 = { by axiom 1 (ax2) R->L }
% 1.21/0.51 sorti1(unit1)
% 1.21/0.51
% 1.21/0.51 Lemma 25: ifeq(sorti1(X), sorti1(unit1), sorti2(h(X)), sorti1(unit1)) = sorti1(unit1).
% 1.21/0.51 Proof:
% 1.21/0.51 ifeq(sorti1(X), sorti1(unit1), sorti2(h(X)), sorti1(unit1))
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq(sorti1(X), sorti1(v3), sorti2(h(X)), sorti1(unit1))
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq(sorti1(X), sorti1(v3), sorti2(h(X)), sorti1(v3))
% 1.21/0.51 = { by lemma 23 }
% 1.21/0.51 ifeq(sorti1(X), sorti2(unit2), sorti2(h(X)), sorti1(v3))
% 1.21/0.51 = { by lemma 23 }
% 1.21/0.51 ifeq(sorti1(X), sorti2(unit2), sorti2(h(X)), sorti2(unit2))
% 1.21/0.51 = { by axiom 2 (ax4) }
% 1.21/0.51 ifeq(sorti1(X), sorti2(v2), sorti2(h(X)), sorti2(unit2))
% 1.21/0.51 = { by axiom 2 (ax4) }
% 1.21/0.51 ifeq(sorti1(X), sorti2(v2), sorti2(h(X)), sorti2(v2))
% 1.21/0.51 = { by axiom 3 (ax4_1) }
% 1.21/0.51 ifeq(sorti1(X), true, sorti2(h(X)), sorti2(v2))
% 1.21/0.51 = { by axiom 3 (ax4_1) }
% 1.21/0.51 ifeq(sorti1(X), true, sorti2(h(X)), true)
% 1.21/0.51 = { by axiom 12 (co1) }
% 1.21/0.51 true
% 1.21/0.51 = { by axiom 3 (ax4_1) R->L }
% 1.21/0.51 sorti2(v2)
% 1.21/0.51 = { by axiom 2 (ax4) R->L }
% 1.21/0.51 sorti2(unit2)
% 1.21/0.51 = { by lemma 23 R->L }
% 1.21/0.51 sorti1(v3)
% 1.21/0.51 = { by axiom 1 (ax2) R->L }
% 1.21/0.51 sorti1(unit1)
% 1.21/0.51
% 1.21/0.51 Lemma 26: sorti2(h(v3)) = sorti1(unit1).
% 1.21/0.51 Proof:
% 1.21/0.51 sorti2(h(v3))
% 1.21/0.51 = { by axiom 7 (ifeq_axiom) R->L }
% 1.21/0.51 ifeq(sorti1(unit1), sorti1(unit1), sorti2(h(v3)), sorti1(unit1))
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq(sorti1(v3), sorti1(unit1), sorti2(h(v3)), sorti1(unit1))
% 1.21/0.51 = { by lemma 25 }
% 1.21/0.51 sorti1(unit1)
% 1.21/0.51
% 1.21/0.51 Lemma 27: sorti2(h(u)) = sorti1(unit1).
% 1.21/0.51 Proof:
% 1.21/0.51 sorti2(h(u))
% 1.21/0.51 = { by axiom 7 (ifeq_axiom) R->L }
% 1.21/0.51 ifeq(sorti1(unit1), sorti1(unit1), sorti2(h(u)), sorti1(unit1))
% 1.21/0.51 = { by lemma 24 R->L }
% 1.21/0.51 ifeq(sorti1(u), sorti1(unit1), sorti2(h(u)), sorti1(unit1))
% 1.21/0.51 = { by lemma 25 }
% 1.21/0.51 sorti1(unit1)
% 1.21/0.51
% 1.21/0.51 Lemma 28: ifeq2(sorti1(X), sorti1(unit1), j(h(X)), X) = X.
% 1.21/0.51 Proof:
% 1.21/0.51 ifeq2(sorti1(X), sorti1(unit1), j(h(X)), X)
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq2(sorti1(X), sorti1(v3), j(h(X)), X)
% 1.21/0.51 = { by lemma 23 }
% 1.21/0.51 ifeq2(sorti1(X), sorti2(unit2), j(h(X)), X)
% 1.21/0.51 = { by axiom 2 (ax4) }
% 1.21/0.51 ifeq2(sorti1(X), sorti2(v2), j(h(X)), X)
% 1.21/0.51 = { by axiom 3 (ax4_1) }
% 1.21/0.51 ifeq2(sorti1(X), true, j(h(X)), X)
% 1.21/0.51 = { by axiom 15 (co1_2) }
% 1.21/0.51 X
% 1.21/0.51
% 1.21/0.51 Lemma 29: j(h(v3)) = v3.
% 1.21/0.51 Proof:
% 1.21/0.51 j(h(v3))
% 1.21/0.51 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.51 ifeq2(sorti1(unit1), sorti1(unit1), j(h(v3)), v3)
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq2(sorti1(v3), sorti1(unit1), j(h(v3)), v3)
% 1.21/0.51 = { by lemma 28 }
% 1.21/0.51 v3
% 1.21/0.51
% 1.21/0.51 Lemma 30: sorti2(w(h(u))) = sorti1(unit1).
% 1.21/0.51 Proof:
% 1.21/0.51 sorti2(w(h(u)))
% 1.21/0.51 = { by axiom 7 (ifeq_axiom) R->L }
% 1.21/0.51 ifeq(sorti1(unit1), sorti1(unit1), sorti2(w(h(u))), sorti1(unit1))
% 1.21/0.51 = { by lemma 27 R->L }
% 1.21/0.51 ifeq(sorti2(h(u)), sorti1(unit1), sorti2(w(h(u))), sorti1(unit1))
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq(sorti2(h(u)), sorti1(v3), sorti2(w(h(u))), sorti1(unit1))
% 1.21/0.51 = { by axiom 1 (ax2) }
% 1.21/0.51 ifeq(sorti2(h(u)), sorti1(v3), sorti2(w(h(u))), sorti1(v3))
% 1.21/0.51 = { by lemma 23 }
% 1.21/0.51 ifeq(sorti2(h(u)), sorti2(unit2), sorti2(w(h(u))), sorti1(v3))
% 1.21/0.51 = { by lemma 23 }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(unit2), sorti2(w(h(u))), sorti2(unit2))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(v2), sorti2(w(h(u))), sorti2(unit2))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(v2), sorti2(w(h(u))), sorti2(v2))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq(sorti2(h(u)), true, sorti2(w(h(u))), sorti2(v2))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq(sorti2(h(u)), true, sorti2(w(h(u))), true)
% 1.21/0.52 = { by axiom 10 (ax8_3) }
% 1.21/0.52 true
% 1.21/0.52 = { by axiom 3 (ax4_1) R->L }
% 1.21/0.52 sorti2(v2)
% 1.21/0.52 = { by axiom 2 (ax4) R->L }
% 1.21/0.52 sorti2(unit2)
% 1.21/0.52 = { by lemma 23 R->L }
% 1.21/0.52 sorti1(v3)
% 1.21/0.52 = { by axiom 1 (ax2) R->L }
% 1.21/0.52 sorti1(unit1)
% 1.21/0.52
% 1.21/0.52 Lemma 31: sorti2(v(h(u))) = sorti1(unit1).
% 1.21/0.52 Proof:
% 1.21/0.52 sorti2(v(h(u)))
% 1.21/0.52 = { by axiom 7 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq(sorti1(unit1), sorti1(unit1), sorti2(v(h(u))), sorti1(unit1))
% 1.21/0.52 = { by lemma 27 R->L }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti1(unit1), sorti2(v(h(u))), sorti1(unit1))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti1(v3), sorti2(v(h(u))), sorti1(unit1))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti1(v3), sorti2(v(h(u))), sorti1(v3))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(unit2), sorti2(v(h(u))), sorti1(v3))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(unit2), sorti2(v(h(u))), sorti2(unit2))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(v2), sorti2(v(h(u))), sorti2(unit2))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq(sorti2(h(u)), sorti2(v2), sorti2(v(h(u))), sorti2(v2))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq(sorti2(h(u)), true, sorti2(v(h(u))), sorti2(v2))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq(sorti2(h(u)), true, sorti2(v(h(u))), true)
% 1.21/0.52 = { by axiom 9 (ax8_2) }
% 1.21/0.52 true
% 1.21/0.52 = { by axiom 3 (ax4_1) R->L }
% 1.21/0.52 sorti2(v2)
% 1.21/0.52 = { by axiom 2 (ax4) R->L }
% 1.21/0.52 sorti2(unit2)
% 1.21/0.52 = { by lemma 23 R->L }
% 1.21/0.52 sorti1(v3)
% 1.21/0.52 = { by axiom 1 (ax2) R->L }
% 1.21/0.52 sorti1(unit1)
% 1.21/0.52
% 1.21/0.52 Lemma 32: op2(h(v3), v2) = h(v3).
% 1.21/0.52 Proof:
% 1.21/0.52 op2(h(v3), v2)
% 1.21/0.52 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq2(sorti1(unit1), sorti1(unit1), op2(h(v3), v2), h(v3))
% 1.21/0.52 = { by lemma 26 R->L }
% 1.21/0.52 ifeq2(sorti2(h(v3)), sorti1(unit1), op2(h(v3), v2), h(v3))
% 1.21/0.52 = { by axiom 2 (ax4) R->L }
% 1.21/0.52 ifeq2(sorti2(h(v3)), sorti1(unit1), op2(h(v3), unit2), h(v3))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq2(sorti2(h(v3)), sorti1(v3), op2(h(v3), unit2), h(v3))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq2(sorti2(h(v3)), sorti2(unit2), op2(h(v3), unit2), h(v3))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq2(sorti2(h(v3)), sorti2(v2), op2(h(v3), unit2), h(v3))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq2(sorti2(h(v3)), true, op2(h(v3), unit2), h(v3))
% 1.21/0.52 = { by axiom 14 (ax4_2) }
% 1.21/0.52 h(v3)
% 1.21/0.52
% 1.21/0.52 Lemma 33: ifeq(sorti2(X), sorti1(unit1), sorti1(j(X)), sorti1(unit1)) = sorti1(unit1).
% 1.21/0.52 Proof:
% 1.21/0.52 ifeq(sorti2(X), sorti1(unit1), sorti1(j(X)), sorti1(unit1))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq(sorti2(X), sorti1(v3), sorti1(j(X)), sorti1(unit1))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq(sorti2(X), sorti1(v3), sorti1(j(X)), sorti1(v3))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq(sorti2(X), sorti2(unit2), sorti1(j(X)), sorti1(v3))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq(sorti2(X), sorti2(unit2), sorti1(j(X)), sorti2(unit2))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq(sorti2(X), sorti2(v2), sorti1(j(X)), sorti2(unit2))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq(sorti2(X), sorti2(v2), sorti1(j(X)), sorti2(v2))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq(sorti2(X), true, sorti1(j(X)), sorti2(v2))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq(sorti2(X), true, sorti1(j(X)), true)
% 1.21/0.52 = { by axiom 11 (co1_3) }
% 1.21/0.52 true
% 1.21/0.52 = { by axiom 3 (ax4_1) R->L }
% 1.21/0.52 sorti2(v2)
% 1.21/0.52 = { by axiom 2 (ax4) R->L }
% 1.21/0.52 sorti2(unit2)
% 1.21/0.52 = { by lemma 23 R->L }
% 1.21/0.52 sorti1(v3)
% 1.21/0.52 = { by axiom 1 (ax2) R->L }
% 1.21/0.52 sorti1(unit1)
% 1.21/0.52
% 1.21/0.52 Lemma 34: sorti1(j(v(h(u)))) = sorti1(unit1).
% 1.21/0.52 Proof:
% 1.21/0.52 sorti1(j(v(h(u))))
% 1.21/0.52 = { by axiom 7 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq(sorti1(unit1), sorti1(unit1), sorti1(j(v(h(u)))), sorti1(unit1))
% 1.21/0.52 = { by lemma 31 R->L }
% 1.21/0.52 ifeq(sorti2(v(h(u))), sorti1(unit1), sorti1(j(v(h(u)))), sorti1(unit1))
% 1.21/0.52 = { by lemma 33 }
% 1.21/0.52 sorti1(unit1)
% 1.21/0.52
% 1.21/0.52 Lemma 35: op2(v(h(u)), w(h(u))) = h(u).
% 1.21/0.52 Proof:
% 1.21/0.52 op2(v(h(u)), w(h(u)))
% 1.21/0.52 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq2(sorti1(unit1), sorti1(unit1), op2(v(h(u)), w(h(u))), h(u))
% 1.21/0.52 = { by lemma 27 R->L }
% 1.21/0.52 ifeq2(sorti2(h(u)), sorti1(unit1), op2(v(h(u)), w(h(u))), h(u))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq2(sorti2(h(u)), sorti1(v3), op2(v(h(u)), w(h(u))), h(u))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq2(sorti2(h(u)), sorti2(unit2), op2(v(h(u)), w(h(u))), h(u))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq2(sorti2(h(u)), sorti2(v2), op2(v(h(u)), w(h(u))), h(u))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq2(sorti2(h(u)), true, op2(v(h(u)), w(h(u))), h(u))
% 1.21/0.52 = { by axiom 18 (ax8_1) }
% 1.21/0.52 h(u)
% 1.21/0.52
% 1.21/0.52 Lemma 36: ifeq2(sorti2(X), sorti1(unit1), ifeq2(sorti2(Y), sorti1(unit1), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X))) = j(op2(Y, X)).
% 1.21/0.52 Proof:
% 1.21/0.52 ifeq2(sorti2(X), sorti1(unit1), ifeq2(sorti2(Y), sorti1(unit1), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq2(sorti2(X), sorti1(v3), ifeq2(sorti2(Y), sorti1(unit1), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 1 (ax2) }
% 1.21/0.52 ifeq2(sorti2(X), sorti1(v3), ifeq2(sorti2(Y), sorti1(v3), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq2(sorti2(X), sorti2(unit2), ifeq2(sorti2(Y), sorti1(v3), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by lemma 23 }
% 1.21/0.52 ifeq2(sorti2(X), sorti2(unit2), ifeq2(sorti2(Y), sorti2(unit2), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq2(sorti2(X), sorti2(v2), ifeq2(sorti2(Y), sorti2(unit2), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 2 (ax4) }
% 1.21/0.52 ifeq2(sorti2(X), sorti2(v2), ifeq2(sorti2(Y), sorti2(v2), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq2(sorti2(X), true, ifeq2(sorti2(Y), sorti2(v2), op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 3 (ax4_1) }
% 1.21/0.52 ifeq2(sorti2(X), true, ifeq2(sorti2(Y), true, op1(j(Y), j(X)), j(op2(Y, X))), j(op2(Y, X)))
% 1.21/0.52 = { by axiom 20 (co1_4) }
% 1.21/0.52 j(op2(Y, X))
% 1.21/0.52
% 1.21/0.52 Lemma 37: op1(j(v(h(u))), u) = j(w(h(u))).
% 1.21/0.52 Proof:
% 1.21/0.52 op1(j(v(h(u))), u)
% 1.21/0.52 = { by axiom 6 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u))))
% 1.21/0.52 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq2(sorti1(unit1), sorti1(unit1), ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by lemma 34 R->L }
% 1.21/0.52 ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.52 ifeq2(sorti1(unit1), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by lemma 33 R->L }
% 1.21/0.52 ifeq2(ifeq(sorti2(w(h(u))), sorti1(unit1), sorti1(j(w(h(u)))), sorti1(unit1)), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by lemma 30 }
% 1.21/0.52 ifeq2(ifeq(sorti1(unit1), sorti1(unit1), sorti1(j(w(h(u)))), sorti1(unit1)), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by axiom 7 (ifeq_axiom) }
% 1.21/0.52 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(u, u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by lemma 28 R->L }
% 1.21/0.52 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti1(unit1), j(h(u)), u), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by lemma 24 }
% 1.21/0.52 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti1(unit1), sorti1(unit1), j(h(u)), u), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by axiom 8 (ifeq_axiom) }
% 1.21/0.52 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(j(h(u)), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.52 = { by lemma 35 R->L }
% 1.21/0.52 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(j(op2(v(h(u)), w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by lemma 36 R->L }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti2(w(h(u))), sorti1(unit1), ifeq2(sorti2(v(h(u))), sorti1(unit1), op1(j(v(h(u))), j(w(h(u)))), j(op2(v(h(u)), w(h(u))))), j(op2(v(h(u)), w(h(u))))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by lemma 35 }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti2(w(h(u))), sorti1(unit1), ifeq2(sorti2(v(h(u))), sorti1(unit1), op1(j(v(h(u))), j(w(h(u)))), j(h(u))), j(op2(v(h(u)), w(h(u))))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by lemma 30 }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti1(unit1), sorti1(unit1), ifeq2(sorti2(v(h(u))), sorti1(unit1), op1(j(v(h(u))), j(w(h(u)))), j(h(u))), j(op2(v(h(u)), w(h(u))))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 8 (ifeq_axiom) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti2(v(h(u))), sorti1(unit1), op1(j(v(h(u))), j(w(h(u)))), j(h(u))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by lemma 31 }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(ifeq2(sorti1(unit1), sorti1(unit1), op1(j(v(h(u))), j(w(h(u)))), j(h(u))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 8 (ifeq_axiom) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 1 (ax2) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(v3), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 1 (ax2) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti1(v3), ifeq2(sorti1(j(v(h(u)))), sorti1(v3), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by lemma 23 }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti2(unit2), ifeq2(sorti1(j(v(h(u)))), sorti1(v3), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by lemma 23 }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti2(unit2), ifeq2(sorti1(j(v(h(u)))), sorti2(unit2), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 2 (ax4) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti2(v2), ifeq2(sorti1(j(v(h(u)))), sorti2(unit2), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 2 (ax4) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), sorti2(v2), ifeq2(sorti1(j(v(h(u)))), sorti2(v2), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 3 (ax4_1) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), true, ifeq2(sorti1(j(v(h(u)))), sorti2(v2), ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 3 (ax4_1) }
% 1.21/0.53 ifeq2(sorti1(j(w(h(u)))), true, ifeq2(sorti1(j(v(h(u)))), true, ifeq3(op1(j(v(h(u))), j(w(h(u)))), u, op1(j(v(h(u))), u), j(w(h(u)))), j(w(h(u)))), j(w(h(u))))
% 1.21/0.53 = { by axiom 21 (ax7_2) }
% 1.21/0.53 j(w(h(u)))
% 1.21/0.53
% 1.21/0.53 Lemma 38: ifeq2(sorti2(X), sorti1(unit1), h(j(X)), X) = X.
% 1.21/0.53 Proof:
% 1.21/0.53 ifeq2(sorti2(X), sorti1(unit1), h(j(X)), X)
% 1.21/0.53 = { by axiom 1 (ax2) }
% 1.21/0.53 ifeq2(sorti2(X), sorti1(v3), h(j(X)), X)
% 1.21/0.53 = { by lemma 23 }
% 1.21/0.53 ifeq2(sorti2(X), sorti2(unit2), h(j(X)), X)
% 1.21/0.53 = { by axiom 2 (ax4) }
% 1.21/0.53 ifeq2(sorti2(X), sorti2(v2), h(j(X)), X)
% 1.21/0.53 = { by axiom 3 (ax4_1) }
% 1.21/0.53 ifeq2(sorti2(X), true, h(j(X)), X)
% 1.21/0.53 = { by axiom 13 (co1_5) }
% 1.21/0.53 X
% 1.21/0.53
% 1.21/0.53 Goal 1 (ax7_1): tuple(u, op1(X, Y), sorti1(X), sorti1(Y)) = tuple(unit1, u, true, true).
% 1.21/0.53 The goal is true when:
% 1.21/0.53 X = u
% 1.21/0.53 Y = v3
% 1.21/0.53
% 1.21/0.53 Proof:
% 1.21/0.53 tuple(u, op1(u, v3), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.53 tuple(u, ifeq2(sorti1(unit1), sorti1(unit1), op1(u, v3), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by lemma 24 R->L }
% 1.21/0.53 tuple(u, ifeq2(sorti1(u), sorti1(unit1), op1(u, v3), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by axiom 1 (ax2) R->L }
% 1.21/0.53 tuple(u, ifeq2(sorti1(u), sorti1(unit1), op1(u, unit1), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by axiom 1 (ax2) }
% 1.21/0.53 tuple(u, ifeq2(sorti1(u), sorti1(v3), op1(u, unit1), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by lemma 23 }
% 1.21/0.53 tuple(u, ifeq2(sorti1(u), sorti2(unit2), op1(u, unit1), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by axiom 2 (ax4) }
% 1.21/0.53 tuple(u, ifeq2(sorti1(u), sorti2(v2), op1(u, unit1), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by axiom 3 (ax4_1) }
% 1.21/0.53 tuple(u, ifeq2(sorti1(u), true, op1(u, unit1), u), sorti1(u), sorti1(v3))
% 1.21/0.53 = { by axiom 16 (ax2_2) }
% 1.21/0.53 tuple(u, u, sorti1(u), sorti1(v3))
% 1.21/0.53 = { by lemma 24 }
% 1.21/0.53 tuple(u, u, sorti1(unit1), sorti1(v3))
% 1.21/0.53 = { by axiom 1 (ax2) R->L }
% 1.21/0.53 tuple(u, u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by lemma 28 R->L }
% 1.21/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(h(u)), u), u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by axiom 6 (ifeq_axiom) R->L }
% 1.21/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq3(w(h(u)), w(h(u)), h(u), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by axiom 8 (ifeq_axiom) R->L }
% 1.21/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti1(unit1), sorti1(unit1), ifeq3(w(h(u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by lemma 27 R->L }
% 1.21/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(w(h(u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by lemma 38 R->L }
% 1.21/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti2(w(h(u))), sorti1(unit1), h(j(w(h(u)))), w(h(u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by lemma 30 }
% 1.21/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(unit1), sorti1(unit1), h(j(w(h(u)))), w(h(u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 1.21/0.53 = { by axiom 8 (ifeq_axiom) }
% 2.00/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(h(j(w(h(u)))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.53 = { by lemma 37 R->L }
% 2.00/0.53 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(h(op1(j(v(h(u))), u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.53 = { by axiom 22 (co1_1) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), true, ifeq2(sorti1(j(v(h(u)))), true, op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 3 (ax4_1) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), true, ifeq2(sorti1(j(v(h(u)))), sorti2(v2), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 3 (ax4_1) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti2(v2), ifeq2(sorti1(j(v(h(u)))), sorti2(v2), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti2(v2), ifeq2(sorti1(j(v(h(u)))), sorti2(unit2), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti2(unit2), ifeq2(sorti1(j(v(h(u)))), sorti2(unit2), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 23 R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti2(unit2), ifeq2(sorti1(j(v(h(u)))), sorti1(v3), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 23 R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti1(v3), ifeq2(sorti1(j(v(h(u)))), sorti1(v3), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 1 (ax2) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti1(v3), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 1 (ax2) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), op2(h(j(v(h(u)))), h(u)), h(op1(j(v(h(u))), u))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 37 }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(u), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), op2(h(j(v(h(u)))), h(u)), h(j(w(h(u))))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 24 }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(unit1), sorti1(unit1), ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), op2(h(j(v(h(u)))), h(u)), h(j(w(h(u))))), h(op1(j(v(h(u))), u))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 8 (ifeq_axiom) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(j(v(h(u)))), sorti1(unit1), op2(h(j(v(h(u)))), h(u)), h(j(w(h(u))))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 34 }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(ifeq2(sorti1(unit1), sorti1(unit1), op2(h(j(v(h(u)))), h(u)), h(j(w(h(u))))), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 8 (ifeq_axiom) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(op2(h(j(v(h(u)))), h(u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 8 (ifeq_axiom) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(op2(ifeq2(sorti1(unit1), sorti1(unit1), h(j(v(h(u)))), v(h(u))), h(u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 31 R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(op2(ifeq2(sorti2(v(h(u))), sorti1(unit1), h(j(v(h(u)))), v(h(u))), h(u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 38 }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), v2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), unit2), v2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(unit1), ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), unit2), unit2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 1 (ax2) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti1(v3), ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), unit2), unit2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 23 }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti2(unit2), ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), unit2), unit2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), sorti2(v2), ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), unit2), unit2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 3 (ax4_1) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(ifeq2(sorti2(h(u)), true, ifeq3(op2(v(h(u)), h(u)), w(h(u)), h(u), unit2), unit2)), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 19 (ax8) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(unit2), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) }
% 2.00/0.54 tuple(ifeq2(sorti1(u), sorti1(unit1), j(v2), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 24 }
% 2.00/0.54 tuple(ifeq2(sorti1(unit1), sorti1(unit1), j(v2), u), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 8 (ifeq_axiom) }
% 2.00/0.54 tuple(j(v2), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 17 (ax2_3) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(j(v2)), true, op1(unit1, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 3 (ax4_1) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(j(v2)), sorti2(v2), op1(unit1, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(j(v2)), sorti2(unit2), op1(unit1, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 23 R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(j(v2)), sorti1(v3), op1(unit1, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 1 (ax2) R->L }
% 2.00/0.54 tuple(ifeq2(sorti1(j(v2)), sorti1(unit1), op1(unit1, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 1 (ax2) }
% 2.00/0.54 tuple(ifeq2(sorti1(j(v2)), sorti1(unit1), op1(v3, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 7 (ifeq_axiom) R->L }
% 2.00/0.54 tuple(ifeq2(ifeq(sorti1(unit1), sorti1(unit1), sorti1(j(v2)), sorti1(unit1)), sorti1(unit1), op1(v3, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 1 (ax2) }
% 2.00/0.54 tuple(ifeq2(ifeq(sorti1(v3), sorti1(unit1), sorti1(j(v2)), sorti1(unit1)), sorti1(unit1), op1(v3, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 23 }
% 2.00/0.54 tuple(ifeq2(ifeq(sorti2(unit2), sorti1(unit1), sorti1(j(v2)), sorti1(unit1)), sorti1(unit1), op1(v3, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by axiom 2 (ax4) }
% 2.00/0.54 tuple(ifeq2(ifeq(sorti2(v2), sorti1(unit1), sorti1(j(v2)), sorti1(unit1)), sorti1(unit1), op1(v3, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.54 = { by lemma 33 }
% 2.00/0.55 tuple(ifeq2(sorti1(unit1), sorti1(unit1), op1(v3, j(v2)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by axiom 8 (ifeq_axiom) }
% 2.00/0.55 tuple(op1(v3, j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 29 R->L }
% 2.00/0.55 tuple(op1(j(h(v3)), j(v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by axiom 8 (ifeq_axiom) R->L }
% 2.00/0.55 tuple(ifeq2(sorti1(unit1), sorti1(unit1), op1(j(h(v3)), j(v2)), j(h(v3))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 26 R->L }
% 2.00/0.55 tuple(ifeq2(sorti2(h(v3)), sorti1(unit1), op1(j(h(v3)), j(v2)), j(h(v3))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by axiom 8 (ifeq_axiom) R->L }
% 2.00/0.55 tuple(ifeq2(sorti1(unit1), sorti1(unit1), ifeq2(sorti2(h(v3)), sorti1(unit1), op1(j(h(v3)), j(v2)), j(h(v3))), j(op2(h(v3), v2))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by axiom 1 (ax2) }
% 2.00/0.55 tuple(ifeq2(sorti1(v3), sorti1(unit1), ifeq2(sorti2(h(v3)), sorti1(unit1), op1(j(h(v3)), j(v2)), j(h(v3))), j(op2(h(v3), v2))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 23 }
% 2.00/0.55 tuple(ifeq2(sorti2(unit2), sorti1(unit1), ifeq2(sorti2(h(v3)), sorti1(unit1), op1(j(h(v3)), j(v2)), j(h(v3))), j(op2(h(v3), v2))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by axiom 2 (ax4) }
% 2.00/0.55 tuple(ifeq2(sorti2(v2), sorti1(unit1), ifeq2(sorti2(h(v3)), sorti1(unit1), op1(j(h(v3)), j(v2)), j(h(v3))), j(op2(h(v3), v2))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 32 R->L }
% 2.00/0.55 tuple(ifeq2(sorti2(v2), sorti1(unit1), ifeq2(sorti2(h(v3)), sorti1(unit1), op1(j(h(v3)), j(v2)), j(op2(h(v3), v2))), j(op2(h(v3), v2))), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 36 }
% 2.00/0.55 tuple(j(op2(h(v3), v2)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 32 }
% 2.00/0.55 tuple(j(h(v3)), u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by lemma 29 }
% 2.00/0.55 tuple(v3, u, sorti1(unit1), sorti1(unit1))
% 2.00/0.55 = { by axiom 1 (ax2) }
% 2.00/0.55 tuple(v3, u, sorti1(v3), sorti1(unit1))
% 2.00/0.55 = { by axiom 1 (ax2) }
% 2.00/0.55 tuple(v3, u, sorti1(v3), sorti1(v3))
% 2.00/0.55 = { by lemma 23 }
% 2.00/0.55 tuple(v3, u, sorti2(unit2), sorti1(v3))
% 2.00/0.55 = { by lemma 23 }
% 2.00/0.55 tuple(v3, u, sorti2(unit2), sorti2(unit2))
% 2.00/0.55 = { by axiom 2 (ax4) }
% 2.00/0.55 tuple(v3, u, sorti2(v2), sorti2(unit2))
% 2.00/0.55 = { by axiom 2 (ax4) }
% 2.00/0.55 tuple(v3, u, sorti2(v2), sorti2(v2))
% 2.00/0.55 = { by axiom 3 (ax4_1) }
% 2.00/0.55 tuple(v3, u, true, sorti2(v2))
% 2.00/0.55 = { by axiom 3 (ax4_1) }
% 2.00/0.55 tuple(v3, u, true, true)
% 2.00/0.55 = { by axiom 1 (ax2) R->L }
% 2.00/0.55 tuple(unit1, u, true, true)
% 2.00/0.55 % SZS output end Proof
% 2.00/0.55
% 2.00/0.55 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------