Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ba9d8.. x0.
Let x1 of type ι → ι be given.
Assume H1: ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0.
Assume H2: ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.
Apply and3I with ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0, ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3, ∀ x2 . prim1 x2 x0 ⟶ ∃ x3 . and (prim1 x3 x0) (x1 x3 = x2) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H3: prim1 x2 x0.
Apply dneg with ∃ x3 . and (prim1 x3 x0) (x1 x3 = x2).
Assume H4: not (∃ x3 . and (prim1 x3 x0) (x1 x3 = x2)).
Apply unknownprop_7a5bcd73ac6de46b7267640d7609e10f55790a2990a70e54b4df80541b8031ef with x0, λ x3 . If_i (x3 = x0) x2 (x1 x3) leaving 3 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H5: prim1 x3 (4ae4a.. x0).
Apply xm with x3 = x0, prim1 (If_i (x3 = x0) x2 (x1 x3)) x0 leaving 2 subgoals.
Assume H6: x3 = x0.
Apply If_i_1 with x3 = x0, x2, x1 x3, λ x4 x5 . prim1 x5 x0 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H3.
Assume H6: x3 = x0 ⟶ ∀ x4 : ο . x4.
Apply If_i_0 with x3 = x0, x2, x1 x3, λ x4 x5 . prim1 x5 x0 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H1 with x3.
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with x0, x3, prim1 x3 x0 leaving 3 subgoals.
The subproof is completed by applying H5.
Assume H7: prim1 x3 x0.
The subproof is completed by applying H7.
Assume H7: x3 = x0.
Apply H6 with prim1 x3 x0.
The subproof is completed by applying H7.
Let x3 of type ι be given.
Assume H5: prim1 x3 (4ae4a.. x0).
Let x4 of type ι be given.
Assume H6: prim1 x4 (4ae4a.. x0).
Claim L7: ...
...
Claim L8: ...
...
Apply xm with x3 = x0, If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 leaving 2 subgoals.
Assume H9: x3 = x0.
Apply xm with x4 = x0, If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 leaving 2 subgoals.
Assume H10: x4 = x0.
Assume H11: If_i (x3 = x0) x2 (x1 x3) = If_i (x4 = x0) x2 (x1 x4).
Apply H10 with λ x5 x6 . x3 = x6.
The subproof is completed by applying H9.
Assume H10: x4 = x0 ⟶ ∀ x5 : ο . x5.
Apply If_i_1 with x3 = x0, x2, x1 x3, λ x5 x6 . x6 = If_i (x4 = x0) x2 (x1 x4) ⟶ x3 = x4 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply If_i_0 with x4 = x0, x2, x1 ..., ... leaving 2 subgoals.
...
...
...
■