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.
Assume H0: ∀ x6 . x6x0x1 x6 = x2 x6.
Assume H1: ∀ x6 . x6x0iff (x3 x6) (x4 x6).
Claim L2: lam x0 x1 = lam x0 x2
Apply encode_u_ext with x0, x1, x2.
The subproof is completed by applying H0.
Apply L2 with λ x6 x7 . lam 4 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) (lam x0 x1) (If_i (x8 = 2) (Sep x0 x3) x5))) = lam 4 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x6 (If_i (x8 = 2) (Sep x0 x4) x5))).
Claim L3: Sep x0 x3 = Sep x0 x4
Apply encode_p_ext with x0, x3, x4.
The subproof is completed by applying H1.
Apply L3 with λ x6 x7 . lam 4 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) (lam x0 x1) (If_i (x8 = 2) (Sep x0 x3) x5))) = lam 4 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) (lam x0 x1) (If_i (x8 = 2) x6 x5))).
Let x6 of type ιιο be given.
Assume H4: x6 (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) (lam x0 x1) (If_i (x7 = 2) (Sep x0 x3) x5)))) (lam 4 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) (lam x0 x1) (If_i (x7 = 2) (Sep x0 x3) x5)))).
The subproof is completed by applying H4.