Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: prim1 ((λ x2 . 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1) x0.
Apply H0 with False.
Let x2 of type ι be given.
Assume H2: (λ x3 . and (ordinal x3) (1beb9.. x3 x0)) x2.
Apply H2 with False.
Assume H3: ordinal x2.
Assume H4: 1beb9.. x2 x0.
Apply H4 with False.
Assume H5: Subq x0 (472ec.. x2).
Apply FalseE with (∀ x3 . prim1 x3 x2 ⟶ exactly1of2 (prim1 (15418.. x3 (91630.. (4ae4a.. 4a7ef..))) x0) (prim1 x3 x0)) ⟶ False.
Claim L6: prim1 ((λ x3 . 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1) (0ac37.. x2 (94f9e.. x2 (λ x3 . (λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3)))
Apply H5 with (λ x3 . 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1.
The subproof is completed by applying H1.
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with x2, 94f9e.. x2 (λ x3 . (λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3), (λ x3 . 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1, False leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7: prim1 ((λ x3 . 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1) x2.
Apply unknownprop_b460e770adfc2e6ce2e9189dcc4056aa82e881b92ae7579bb723ddb431802d04 with x2, x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Assume H7: prim1 ((λ x3 . 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1) (94f9e.. x2 (λ x3 . (λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x2, λ x3 . (λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3, (λ x3 . 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1, False leaving 2 subgoals.
The subproof is completed by applying H7.
Let x3 of type ι be given.
Assume H8: prim1 x3 x2.
Assume H9: (λ x4 . 15418.. x4 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1 = (λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3.
Claim L10: ordinal x3
Apply ordinal_Hered with x2, x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H8.
Claim L11: prim1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) ((λ x4 . 15418.. x4 (91630.. (4ae4a.. 4a7ef..))) x3)
Apply H9 with λ x4 x5 . prim1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) x4.
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with x1, 91630.. (91630.. (4ae4a.. (4ae4a.. 4a7ef..))), 91630.. (4ae4a.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with 91630.. (4ae4a.. (4ae4a.. 4a7ef..)).
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with x3, 91630.. (91630.. (4ae4a.. 4a7ef..)), 91630.. (4ae4a.. (4ae4a.. 4a7ef..)), False leaving 3 subgoals.
The subproof is completed by applying L11.
Assume H12: prim1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) x3.
Apply unknownprop_233a01ed74afb32f65afd3e8784abd0a97273e5d2c2787b08adfb08e640439ec.
Apply ordinal_Hered with x3, 91630.. (4ae4a.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying H12.
The subproof is completed by applying unknownprop_e87260b1013ba25c00e71f0b980f91b6ef632a8abaf76671d652722aaa34ef37.
■