Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type (ιο) → ο be given.
Let x2 of type (ιο) → ο be given.
Let x3 of type ιι be given.
Let x4 of type ιι be given.
Let x5 of type ιιο be given.
Let x6 of type ιιο be given.
Let x7 of type ιο be given.
Let x8 of type ιο be given.
Assume H0: ∀ x9 : ι → ο . (∀ x10 . x9 x10x10x0)iff (x1 x9) (x2 x9).
Assume H1: ∀ x9 . x9x0x3 x9 = x4 x9.
Assume H2: ∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x6 x9 x10).
Assume H3: ∀ x9 . x9x0iff (x7 x9) (x8 x9).
Claim L4: ...
...
Apply L4 with λ x9 x10 . lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) (encode_c x0 x1) (If_i (x11 = 2) (lam x0 x3) (If_i (x11 = 3) (encode_r x0 x5) (Sep x0 x7))))) = lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) x9 (If_i (x11 = 2) (lam x0 x4) (If_i (x11 = 3) (encode_r x0 x6) (Sep x0 x8))))).
Claim L5: ...
...
Apply L5 with λ x9 x10 . lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) (encode_c x0 x1) (If_i (x11 = 2) (lam x0 x3) (If_i (x11 = 3) (encode_r x0 x5) (Sep x0 x7))))) = lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) (encode_c x0 x1) (If_i (x11 = 2) x9 (If_i (x11 = 3) (encode_r x0 x6) (Sep x0 x8))))).
Claim L6: ...
...
Apply L6 with λ x9 x10 . lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) (encode_c x0 x1) (If_i (x11 = 2) (lam x0 x3) (If_i (x11 = 3) (encode_r x0 x5) (Sep x0 x7))))) = lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) (encode_c x0 x1) (If_i (x11 = 2) (lam x0 x3) (If_i (x11 = 3) x9 (Sep x0 x8))))).
Claim L7: ...
...
Apply L7 with λ x9 x10 . lam 5 (λ x11 . If_i (x11 = 0) x0 (If_i (x11 = 1) (encode_c x0 x1) (If_i (x11 = 2) (lam x0 x3) (If_i (... = 3) ... ...)))) = ....
...