Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιιιο be given.
Assume H0: ∀ x1 x2 x3 . 80242.. x180242.. x280242.. x3(∀ x4 . prim1 x4 (56ded.. (e4431.. x1))x0 x4 x2 x3)(∀ x4 . prim1 x4 (56ded.. (e4431.. x2))x0 x1 x4 x3)(∀ x4 . prim1 x4 (56ded.. (e4431.. x3))x0 x1 x2 x4)(∀ x4 . prim1 x4 (56ded.. (e4431.. x1))∀ x5 . prim1 x5 (56ded.. (e4431.. x2))x0 x4 x5 x3)(∀ x4 . prim1 x4 (56ded.. (e4431.. x1))∀ x5 . prim1 x5 (56ded.. (e4431.. x3))x0 x4 x2 x5)(∀ x4 . prim1 x4 (56ded.. (e4431.. x2))∀ x5 . prim1 x5 (56ded.. (e4431.. x3))x0 x1 x4 x5)(∀ x4 . prim1 x4 (56ded.. (e4431.. x1))∀ x5 . prim1 x5 (56ded.. (e4431.. x2))∀ x6 . prim1 x6 (56ded.. (e4431.. x3))x0 x4 x5 x6)x0 x1 x2 x3.
Claim L1: ∀ 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
Apply ordinal_ind with λ 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.
Assume H1: ordinal x1.
Assume H2: ∀ x2 . prim1 x2 x1∀ x3 . ordinal x3∀ x4 . ordinal x4∀ x5 . prim1 x5 (56ded.. x2)∀ x6 . prim1 x6 (56ded.. x3)∀ x7 . prim1 x7 (56ded.. x4)x0 x5 x6 x7.
Apply ordinal_ind with λ x2 . ∀ x3 . ordinal x3∀ x4 . prim1 x4 (56ded.. x1)∀ x5 . prim1 x5 (56ded.. x2)∀ x6 . prim1 x6 (56ded.. x3)x0 x4 x5 x6.
Let x2 of type ι be given.
Assume H3: ordinal x2.
Assume H4: ∀ x3 . prim1 ... ...∀ x4 . ordinal x4∀ x5 . prim1 x5 (56ded.. x1)∀ x6 . prim1 x6 (56ded.. x3)∀ x7 . prim1 x7 (56ded.. x4)x0 x5 x6 x7.
...
Apply unknownprop_569cb471be0809144fbd3507f3df6cc41b74b600f6043368ffb19c3a241db662 with x0.
The subproof is completed by applying L1.