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 (SNoCutP (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})) (add_SNo x4 x5 = SNoCut (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})).
Assume H4: and (∀ x6 . x6x0SNo x6) (∀ x6 . x6x1SNo x6).
Apply H4 with (∀ x6 . x6x0∀ x7 . x7x1SNoLt x6 x7)and (SNoCutP (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})) (add_SNo x4 x5 = SNoCut (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})).
Assume H5: ∀ x6 . x6x0SNo x6.
Assume H6: ∀ x6 . x6x1SNo x6.
Assume H7: ∀ x6 . x6x0∀ x7 . x7x1SNoLt x6 x7.
Apply H1 with and (SNoCutP (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})) (add_SNo x4 x5 = SNoCut (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})).
Assume H8: and (∀ x6 . x6x2SNo x6) (∀ x6 . x6x3SNo x6).
Apply H8 with ...and (SNoCutP (binunion {add_SNo x6 x5|x6 ∈ x0} {add_SNo x4 x6|x6 ∈ x2}) (binunion {add_SNo x6 x5|x6 ∈ x1} {add_SNo x4 x6|x6 ∈ x3})) (add_SNo x4 x5 = SNoCut (binunion {add_SNo x6 x5|x6 ∈ x0} {...|x6 ∈ ...}) ...).
...