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: SNoCutP x0 x1.
Assume H1: SNoCutP x2 x3.
Assume H2: x4 = SNoCut x0 x1.
Assume H3: x5 = SNoCut x2 x3.
Apply H0 with and (and (SNoCutP (binunion {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x0 x2} {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x1 x3}) (binunion {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x0 x3} {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x1 x2})) (mul_SNo x4 x5 = SNoCut (binunion {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x0 x2} {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x1 x3}) (binunion {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x0 x3} {add_SNo (mul_SNo (ap x6 0) x5) (add_SNo (mul_SNo x4 (ap x6 1)) (minus_SNo (mul_SNo (ap x6 0) (ap x6 1))))|x6 ∈ setprod x1 x2}))) (∀ x6 : ο . (∀ x7 x8 x9 x10 . .....................(∀ x11 . ...∀ x12 . ...add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) ...)...)SNoCutP (binunion x7 x8) (binunion x9 x10)mul_SNo x4 x5 = SNoCut (binunion x7 x8) (binunion x9 x10)x6)x6).
...