Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 . ordinal x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 (56ded.. x1) ⟶ ∀ x4 . prim1 x4 (56ded.. x2) ⟶ x0 x3 x4.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1: 80242.. x1.
Assume H2: 80242.. x2.
Claim L3: ordinal (e4431.. x1)
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x1.
The subproof is completed by applying H1.
Claim L4: ordinal (4ae4a.. (e4431.. x1))
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with e4431.. x1.
The subproof is completed by applying L3.
Claim L5: prim1 x1 (56ded.. (4ae4a.. (e4431.. x1)))
Apply unknownprop_55be23921c8e687561ab6e9faf36ed3618fa021f01ef196ba95aa8fcda0b83ee with x1.
The subproof is completed by applying H1.
Claim L6: ordinal (e4431.. x2)
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x2.
The subproof is completed by applying H2.
Claim L7: ordinal (4ae4a.. (e4431.. x2))
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with e4431.. x2.
The subproof is completed by applying L6.
Claim L8: prim1 x2 (56ded.. (4ae4a.. (e4431.. x2)))
Apply unknownprop_55be23921c8e687561ab6e9faf36ed3618fa021f01ef196ba95aa8fcda0b83ee with x2.
The subproof is completed by applying H2.
Apply H0 with 4ae4a.. (e4431.. x1), 4ae4a.. (e4431.. x2), x1, x2 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L7.
The subproof is completed by applying L5.
The subproof is completed by applying L8.
■