Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with λ x0 . (λ x1 . ∀ x2 . 80242.. x2∀ x3 : ο . (80242.. (e6316.. x1 x2)(∀ x4 . prim1 x4 (23e07.. x1)∀ x5 . prim1 x5 (23e07.. x2)099f3.. (bc82c.. (e6316.. x4 x2) (e6316.. x1 x5)) (bc82c.. (e6316.. x1 x2) (e6316.. x4 x5)))(∀ x4 . prim1 x4 (5246e.. x1)∀ x5 . prim1 x5 (5246e.. x2)099f3.. (bc82c.. (e6316.. x4 x2) (e6316.. x1 x5)) (bc82c.. (e6316.. x1 x2) (e6316.. x4 x5)))(∀ x4 . prim1 x4 (23e07.. x1)∀ x5 . prim1 x5 (5246e.. x2)099f3.. (bc82c.. (e6316.. x1 x2) (e6316.. x4 x5)) (bc82c.. (e6316.. x4 x2) (e6316.. x1 x5)))(∀ x4 . prim1 x4 (5246e.. x1)∀ x5 . prim1 x5 (23e07.. x2)099f3.. (bc82c.. (e6316.. x1 x2) (e6316.. x4 x5)) (bc82c.. (e6316.. x4 x2) (e6316.. x1 x5)))x3)x3) x0.
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: ∀ x1 . prim1 x1 (56ded.. (e4431.. x0))(λ x2 . ∀ x3 . 80242.. x3∀ x4 : ο . (80242.. (e6316.. x2 x3)(∀ x5 . prim1 x5 (23e07.. x2)∀ x6 . prim1 x6 (23e07.. x3)099f3.. (bc82c.. (e6316.. x5 x3) (e6316.. x2 x6)) (bc82c.. (e6316.. x2 x3) (e6316.. x5 x6)))(∀ x5 . prim1 x5 (5246e.. x2)∀ x6 . prim1 x6 (5246e.. x3)099f3.. (bc82c.. (e6316.. x5 x3) (e6316.. x2 x6)) (bc82c.. (e6316.. x2 x3) (e6316.. x5 x6)))(∀ x5 . prim1 x5 (23e07.. x2)∀ x6 . prim1 x6 (5246e.. x3)099f3.. (bc82c.. (e6316.. x2 x3) (e6316.. x5 x6)) (bc82c.. (e6316.. x5 x3) (e6316.. x2 x6)))(∀ x5 . prim1 x5 (5246e.. x2)∀ x6 . prim1 x6 (23e07.. x3)099f3.. (bc82c.. (e6316.. x2 x3) (e6316.. x5 x6)) (bc82c.. (e6316.. x5 x3) (e6316.. x2 x6)))x4)x4) x1.
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with λ x1 . (λ x2 . ∀ x3 : ο . (............(∀ x4 . ...∀ x5 . ...099f3.. (bc82c.. (e6316.. x0 x2) (e6316.. x4 x5)) (bc82c.. (e6316.. x4 ...) ...))x3)x3) ....
...