Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoLev x0.
Apply restr_SNo_SNoCut with x0, x1, binintersect (minus_SNo x0) (SNoElts_ x1) = minus_SNo (binintersect x0 (SNoElts_ x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: SNoCutP {x2 ∈ SNoL x0|SNoLev x2 ∈ x1} {x2 ∈ SNoR x0|SNoLev x2 ∈ x1}.
Assume H3: binintersect x0 (SNoElts_ x1) = SNoCut {x2 ∈ SNoL x0|SNoLev x2 ∈ x1} {x2 ∈ SNoR x0|SNoLev x2 ∈ x1}.
Claim L4: ...
...
Claim L5: ...
...
Apply restr_SNo_SNoCut with minus_SNo x0, x1, binintersect (minus_SNo x0) (SNoElts_ x1) = minus_SNo (binintersect x0 (SNoElts_ x1)) leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Assume H6: SNoCutP {x2 ∈ SNoL (minus_SNo x0)|SNoLev x2 ∈ x1} {x2 ∈ SNoR (minus_SNo x0)|SNoLev x2 ∈ x1}.
Assume H7: binintersect (minus_SNo x0) (SNoElts_ x1) = SNoCut {x2 ∈ SNoL (minus_SNo x0)|SNoLev x2 ∈ x1} {x2 ∈ SNoR (minus_SNo x0)|SNoLev x2 ∈ x1}.
Apply H3 with λ x2 x3 . binintersect (minus_SNo x0) (SNoElts_ x1) = minus_SNo x3.
Apply H7 with λ x2 x3 . x3 = minus_SNo (SNoCut {x4 ∈ SNoL x0|SNoLev x4 ∈ x1} {x4 ∈ SNoR x0|SNoLev x4 ∈ x1}).
Apply minus_SNoCut_eq with {x2 ∈ SNoL x0|SNoLev x2 ∈ x1}, {x2 ∈ SNoR x0|SNoLev x2 ∈ x1}, λ x2 x3 . SNoCut {x4 ∈ SNoL (minus_SNo x0)|SNoLev x4 ∈ x1} {x4 ∈ SNoR (minus_SNo x0)|SNoLev x4 ∈ x1} = x3 leaving 2 subgoals.
The subproof is completed by applying H2.
set y2 to be ...
set y3 to be ...
Claim L8: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2
Let x4 of type ι → ο be given.
Assume H8: x4 (SNoCut {minus_SNo x5|x5 ∈ {x5 ∈ SNoR y2|SNoLev x5 ∈ y3}} {minus_SNo x5|x5 ∈ {x5 ∈ SNoL y2|SNoLev x5 ∈ y3}}).
set y5 to be ...
Apply set_ext with {x6 ∈ SNoL (minus_SNo y2)|SNoLev x6 ∈ y3}, {minus_SNo x6|x6 ∈ {x6 ∈ SNoR y2|SNoLev x6 ∈ y3}}, λ x6 x7 . y5 (SNoCut x6 {x8 ∈ SNoR (minus_SNo y2)|SNoLev x8 ∈ y3}) (SNoCut x7 {x8 ∈ SNoR (minus_SNo y2)|SNoLev x8 ∈ y3}) leaving 3 subgoals.
Let x6 of type ι be given.
Assume H9: x6 ∈ {x7 ∈ SNoL (minus_SNo y2)|SNoLev x7 ∈ y3}.
Apply SepE with SNoL (minus_SNo y2), λ x7 . SNoLev x7 ∈ y3, x6, x6 ∈ prim5 {x7 ∈ SNoR y2|...} ... leaving 2 subgoals.
...
...
...
...
Let x4 of type ι → ι → ο be given.
Apply L8 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H9: x4 y3 y3.
The subproof is completed by applying H9.
■