Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: ∀ x1 x2 . 02b90.. x1 x2 ⟶ (∀ x3 . prim1 x3 x1 ⟶ x0 x3) ⟶ (∀ x3 . prim1 x3 x2 ⟶ x0 x3) ⟶ x0 (02a50.. x1 x2).
Claim L1: ∀ x1 . ordinal x1 ⟶ ∀ x2 . 80242.. x2 ⟶ prim1 (e4431.. x2) x1 ⟶ x0 x2
Apply ordinal_ind with λ x1 . ∀ x2 . 80242.. x2 ⟶ prim1 (e4431.. x2) x1 ⟶ x0 x2.
Let x1 of type ι be given.
Assume H1: ordinal x1.
Assume H2: ∀ x2 . prim1 x2 x1 ⟶ ∀ x3 . 80242.. x3 ⟶ prim1 (e4431.. x3) x2 ⟶ x0 x3.
Let x2 of type ι be given.
Assume H3: 80242.. x2.
Assume H4: prim1 (e4431.. x2) x1.
Claim L5: ordinal (e4431.. x2)
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x2.
The subproof is completed by applying H3.
Apply unknownprop_cc3db1e7e6ab5acc021de1f38410cd7fd21abdf75805810622e911337f15975f with x2, x0 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H6: 02b90.. x3 x4.
Assume H7: ∀ x5 . prim1 x5 x3 ⟶ prim1 (e4431.. x5) (e4431.. x2).
Assume H8: ∀ x5 . prim1 x5 x4 ⟶ prim1 (e4431.. x5) (e4431.. x2).
Assume H9: x2 = 02a50.. x3 x4.
Apply H6 with x0 x2.
Assume H10: and (∀ x5 . prim1 x5 x3 ⟶ 80242.. x5) (∀ x5 . prim1 x5 x4 ⟶ 80242.. x5).
Apply H10 with (∀ x5 . prim1 x5 x3 ⟶ ∀ x6 . prim1 x6 x4 ⟶ 099f3.. x5 x6) ⟶ x0 x2.
Assume H11: ∀ x5 . prim1 x5 x3 ⟶ 80242.. x5.
Assume H12: ∀ x5 . prim1 x5 x4 ⟶ 80242.. x5.
Assume H13: ∀ x5 . prim1 x5 x3 ⟶ ∀ x6 . prim1 x6 x4 ⟶ 099f3.. x5 x6.
Apply H9 with λ x5 x6 . x0 x6.
Apply H0 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H14: prim1 x5 x3.
Apply H2 with e4431.. x2, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H11 with x5.
The subproof is completed by applying H14.
Apply H7 with x5.
The subproof is completed by applying H14.
Let x5 of type ι be given.
Assume H14: prim1 x5 x4.
Apply H2 with e4431.. x2, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H12 with x5.
The subproof is completed by applying H14.
Apply H8 with x5.
The subproof is completed by applying H14.
Let x1 of type ι be given.
Assume H2: 80242.. x1.
Claim L3: ordinal (4ae4a.. (e4431.. x1))
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with e4431.. x1.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x1.
The subproof is completed by applying H2.
Apply L1 with 4ae4a.. (e4431.. x1), x1 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with e4431.. x1.
■