Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_85336ee07ace71a942dc508d3b8c851d9d6bb88511443b7dafbf11b71c263f4d with λ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (4ae4a.. x0)prim1 (x1 x2) x0)not (∀ x2 . prim1 x2 (4ae4a.. x0)∀ x3 . prim1 x3 (4ae4a.. x0)x1 x2 = x1 x3x2 = x3) leaving 2 subgoals.
Let x0 of type ιι be given.
Assume H0: ∀ x1 . prim1 x1 (4ae4a.. 4a7ef..)prim1 (x0 x1) 4a7ef...
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0 4a7ef.., not (∀ x1 . prim1 x1 (4ae4a.. 4a7ef..)∀ x2 . prim1 x2 (4ae4a.. 4a7ef..)x0 x1 = x0 x2x1 = x2).
Apply H0 with 4a7ef...
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
Let x0 of type ι be given.
Assume H0: ba9d8.. x0.
Assume H1: ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (4ae4a.. x0)prim1 (x1 x2) x0)not (∀ x2 . prim1 x2 (4ae4a.. x0)∀ x3 . prim1 x3 (4ae4a.. x0)x1 x2 = x1 x3x2 = x3).
Let x1 of type ιι be given.
Assume H2: ∀ x2 . prim1 x2 (4ae4a.. (4ae4a.. x0))prim1 (x1 x2) (4ae4a.. x0).
Assume H3: ∀ x2 . prim1 x2 (4ae4a.. (4ae4a.. x0))∀ x3 . prim1 x3 (4ae4a.. (4ae4a.. x0))x1 x2 = x1 x3x2 = x3.
Apply xm with ∃ x2 . and (prim1 x2 (4ae4a.. (4ae4a.. x0))) (x1 x2 = x0), False leaving 2 subgoals.
Assume H4: ∃ x2 . and (prim1 x2 (4ae4a.. (4ae4a.. x0))) (x1 x2 = x0).
Apply H4 with False.
Let x2 of type ι be given.
Assume H5: (λ x3 . and (prim1 x3 (4ae4a.. (4ae4a.. x0))) (x1 x3 = x0)) x2.
Apply H5 with False.
Assume H6: prim1 x2 (4ae4a.. (4ae4a.. x0)).
Assume H7: x1 x2 = x0.
Apply H1 with λ x3 . If_i (Subq x2 x3) (x1 (4ae4a.. x3)) (x1 x3) leaving 2 subgoals.
Let x3 of type ι be given.
Assume H8: prim1 x3 (4ae4a.. x0).
Apply xm with Subq x2 x3, prim1 ((λ x4 . If_i (Subq x2 x4) (x1 (4ae4a.. x4)) (x1 x4)) x3) x0 leaving 2 subgoals.
Assume H9: Subq x2 x3.
Apply If_i_1 with Subq x2 x3, x1 (4ae4a.. x3), x1 x3, λ x4 x5 . prim1 x5 x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Claim L10: ...
...
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with x0, x1 (4ae4a.. x3), prim1 (x1 (4ae4a.. x3)) x0 leaving 3 subgoals.
Apply H2 with 4ae4a.. x3.
The subproof is completed by applying L10.
Assume H11: prim1 (x1 (4ae4a.. x3)) x0.
The subproof is completed by applying H11.
Assume H11: x1 (4ae4a.. x3) = x0.
Apply FalseE with prim1 (x1 (4ae4a.. x3)) x0.
Apply In_irref with x3.
Claim L12: ...
...
Claim L13: prim1 x3 x2
Apply L12 with λ x4 x5 . prim1 ... ....
...
Apply H9 with x3.
The subproof is completed by applying L13.
...
...
...