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 add_SNoCutP_lem with x0, x1, x2, x3, x4, x5, 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}) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Assume H4: SNoCutP (binunion {add_SNo x6 x5|x6 ∈ x0} (prim5 x2 (add_SNo x4))) (binunion {add_SNo x6 x5|x6 ∈ x1} (prim5 x3 (add_SNo x4))).
Assume H5: add_SNo x4 x5 = SNoCut (binunion {add_SNo x6 x5|x6 ∈ x0} (prim5 x2 (add_SNo x4))) (binunion {add_SNo x6 x5|x6 ∈ x1} (prim5 x3 (add_SNo x4))).
The subproof is completed by applying H5.