Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιιο be given.
Assume H0: ∀ x1 x2 . 80242.. x180242.. x2(∀ x3 . prim1 x3 (56ded.. (e4431.. x1))x0 x3 x2)(∀ x3 . prim1 x3 (56ded.. (e4431.. x2))x0 x1 x3)(∀ x3 . prim1 x3 (56ded.. (e4431.. x1))∀ x4 . prim1 x4 (56ded.. (e4431.. x2))x0 x3 x4)x0 x1 x2.
Claim L1: ∀ x1 . ordinal x1∀ x2 . ordinal x2∀ x3 . prim1 x3 (56ded.. x1)∀ x4 . prim1 x4 (56ded.. x2)x0 x3 x4
Apply ordinal_ind with λ x1 . ∀ x2 . ordinal x2∀ x3 . prim1 x3 (56ded.. x1)∀ x4 . prim1 x4 (56ded.. x2)x0 x3 x4.
Let x1 of type ι be given.
Assume H1: ordinal x1.
Assume H2: ∀ x2 . prim1 x2 x1∀ x3 . ordinal x3∀ x4 . prim1 x4 (56ded.. x2)∀ x5 . prim1 x5 (56ded.. x3)x0 x4 x5.
Apply ordinal_ind with λ x2 . ∀ x3 . prim1 x3 (56ded.. x1)∀ x4 . prim1 x4 (56ded.. x2)x0 x3 x4.
Let x2 of type ι be given.
Assume H3: ordinal x2.
Assume H4: ∀ x3 . prim1 x3 x2∀ x4 . prim1 x4 (56ded.. x1)∀ x5 . prim1 x5 (56ded.. x3)x0 x4 x5.
Let x3 of type ι be given.
Assume H5: prim1 x3 (56ded.. x1).
Let x4 of type ι be given.
Assume H6: prim1 x4 (56ded.. x2).
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with x1, x3, x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Assume H7: prim1 (e4431.. x3) x1.
Assume H8: ordinal (e4431.. x3).
Assume H9: 80242.. x3.
Assume H10: 1beb9.. (e4431.. x3) x3.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with x2, x4, x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Assume H11: prim1 (e4431.. x4) x2.
Assume H12: ordinal (e4431.. x4).
Assume H13: 80242.. x4.
Assume H14: 1beb9.. (e4431.. x4) x4.
Apply H0 with x3, x4 leaving 5 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H13.
Let x5 of type ι be given.
Assume H15: prim1 x5 (56ded.. (e4431.. x3)).
Apply H2 with e4431.. x3, x2, x5, x4 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H3.
The subproof is completed by applying H15.
The subproof is completed by applying H6.
Apply H4 with e4431.. x4, x3 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H5.
Let x5 of type ι be given.
Assume H15: prim1 x5 (56ded.. (e4431.. x3)).
Let x6 of type ι be given.
Assume H16: prim1 x6 (56ded.. (e4431.. x4)).
Apply H2 with e4431.. x3, e4431.. x4, x5, x6 leaving 4 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H12.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
Apply unknownprop_800ab0f9f7d5e23ffc560fa6f3a77275d4dd8d39b4817caedaa494e089e82bfc with x0.
The subproof is completed by applying L1.