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