Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . ...∀ x1 . ...∀ x2 x3 : ι → ι → ι . ......(λ x4 x5 . λ x6 : ι → ι → ι . SNoCut (binunion {add_SNo (x6 (ap x7 0) x5) (add_SNo (x6 x4 (ap x7 1)) (minus_SNo (x6 (ap x7 0) (ap x7 1))))|x7 ∈ setprod (SNoL x4) (SNoL x5)} {add_SNo (x6 (ap x7 0) x5) (add_SNo (x6 x4 (ap x7 1)) (minus_SNo (x6 (ap x7 0) (ap x7 1))))|x7 ∈ setprod (SNoR x4) (SNoR x5)}) (binunion {add_SNo (x6 (ap x7 0) x5) (add_SNo (x6 x4 (ap x7 1)) (minus_SNo (x6 (ap x7 0) (ap x7 1))))|x7 ∈ setprod (SNoL x4) (SNoR x5)} {add_SNo (x6 (ap x7 0) x5) (add_SNo (x6 x4 (ap x7 1)) (minus_SNo (x6 (ap x7 0) (ap x7 1))))|x7 ∈ setprod (SNoR x4) (SNoL x5)})) x0 x1 x2 = (λ x4 x5 . λ x6 : ι → ι → ι . SNoCut (binunion {add_SNo (x6 (ap x7 0) x5) (add_SNo (x6 x4 (ap x7 1)) (minus_SNo (x6 (ap x7 0) (ap x7 1))))|x7 ∈ setprod (SNoL x4) (SNoL x5)} {...|x7 ∈ setprod ... ...}) ...) ... ... ...
...
Apply SNo_rec2_eq with λ x0 x1 . λ x2 : ι → ι → ι . SNoCut (binunion {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoL x0) (SNoL x1)} {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoR x0) (SNoR x1)}) (binunion {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoL x0) (SNoR x1)} {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoR x0) (SNoL x1)}).
The subproof is completed by applying L0.