Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: prim1 (e4431.. x0) (09072.. (4ae4a.. (e4431.. x0)) (λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2))).
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with 1216a.. (4ae4a.. (e4431.. x0)) (λ x1 . (λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3)) x1), a4c2a.. (4ae4a.. (e4431.. x0)) (λ x1 . not ((λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3)) x1)) (λ x1 . (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1), e4431.. x0, False leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: prim1 (e4431.. x0) (1216a.. (4ae4a.. (e4431.. x0)) (λ x1 . (λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3)) x1)).
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with 4ae4a.. (e4431.. x0), λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2), e4431.. x0, False leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3: prim1 (e4431.. x0) x0.
Assume H4: e4431.. x0 = e4431.. x0 ⟶ ∀ x1 : ο . x1.
Apply H4.
Let x1 of type ι → ι → ο be given.
Assume H5: x1 (e4431.. x0) (e4431.. x0).
The subproof is completed by applying H5.
Assume H2: prim1 (e4431.. x0) (a4c2a.. (4ae4a.. (e4431.. x0)) (λ x1 . not ((λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3)) x1)) (λ x1 . (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1)).
Apply unknownprop_e546e9a8cc28c7314a8604ada98e2a83641f2ef6b8078441570ffe037b28d26f with 4ae4a.. (e4431.. x0), λ x1 . not ((λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3)) x1), λ x1 . (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1, e4431.. x0, False leaving 2 subgoals.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H3: prim1 x1 (4ae4a.. (e4431.. x0)).
Assume H4: not ((λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3)) x1).
Assume H5: e4431.. x0 = (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1.
Apply unknownprop_81d5bf525fa56ced1f50f507419c213d2f5baf8a9bd690d88066a9046e094314 with x1.
Apply H5 with λ x2 x3 . ordinal x2.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x0.
The subproof is completed by applying H0.
■