Search for blocks/addresses/...

Proofgold Proof

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