Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ∀ x2 . x2x0SNo x2.
Assume H1: SNo_max_of x0 x1.
Apply H1 with SNo_min_of {minus_SNo x2|x2 ∈ x0} (minus_SNo x1).
Assume H2: and (x1x0) (SNo x1).
Apply H2 with (∀ x2 . x2x0SNo x2SNoLe x2 x1)SNo_min_of {minus_SNo x2|x2 ∈ x0} (minus_SNo x1).
Assume H3: x1x0.
Assume H4: SNo x1.
Assume H5: ∀ x2 . x2x0SNo x2SNoLe x2 x1.
Apply and3I with minus_SNo x1{minus_SNo x2|x2 ∈ x0}, SNo (minus_SNo x1), ∀ x2 . x2{minus_SNo x3|x3 ∈ x0}SNo x2SNoLe (minus_SNo x1) x2 leaving 3 subgoals.
Apply ReplI with x0, minus_SNo, x1.
The subproof is completed by applying H3.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H6: x2{minus_SNo x3|x3 ∈ x0}.
Assume H7: SNo x2.
Apply ReplE_impred with x0, λ x3 . minus_SNo x3, x2, SNoLe (minus_SNo x1) x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H8: x3x0.
Assume H9: x2 = minus_SNo x3.
Apply H9 with λ x4 x5 . SNoLe (minus_SNo x1) x5.
Apply minus_SNo_Le_contra with x3, x1 leaving 3 subgoals.
Apply H0 with x3.
The subproof is completed by applying H8.
The subproof is completed by applying H4.
Apply H5 with x3 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply H0 with x3.
The subproof is completed by applying H8.