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.
Assume H0: SNo x1.
Assume H1: ∀ x4 . x4SNoS_ (SNoLev x0)∀ x5 . SNo x5x2 x4 x5 = x3 x4 x5.
Assume H2: ∀ x4 . x4SNoS_ (SNoLev x1)x2 x0 x4 = x3 x0 x4.
Assume H3: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoL x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoL x1)}.
Assume H4: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoR x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoR x1)}.
Assume H5: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoR x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoR x1)}.
Assume H6: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoL x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoL x1)}.
Apply H3 with λ x4 x5 . SNoCut (binunion x5 {...|x6 ∈ setprod (SNoR x0) (SNoR x1)}) ... = ....
...