Search for blocks/addresses/...

Proofgold Proof

pf
Apply int_SNo_cases with λ x0 . ∀ x1 : ο . (SNoLt x0 0 ⟶ minus_SNo x0 ∈ omega ⟶ x1) ⟶ (SNoLe 0 x0 ⟶ not (SNoLt x0 0) ⟶ x0 ∈ omega ⟶ x1) ⟶ x1 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Claim L1: SNoLe 0 x0
Apply ordinal_Subq_SNoLe with 0, x0 leaving 3 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
The subproof is completed by applying Subq_Empty with x0.
Claim L2: SNo x0
Apply omega_SNo with x0.
The subproof is completed by applying H0.
Let x1 of type ο be given.
Assume H3: SNoLt x0 0 ⟶ minus_SNo x0 ∈ omega ⟶ x1.
Assume H4: SNoLe 0 x0 ⟶ not (SNoLt x0 0) ⟶ x0 ∈ omega ⟶ x1.
Apply H4 leaving 3 subgoals.
The subproof is completed by applying L1.
Assume H5: SNoLt x0 0.
Apply SNoLt_irref with x0.
Apply SNoLtLe_tra with x0, 0, x0 leaving 5 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L2.
The subproof is completed by applying H5.
The subproof is completed by applying L1.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Let x1 of type ο be given.
Assume H1: SNoLt (minus_SNo x0) 0 ⟶ minus_SNo (minus_SNo x0) ∈ omega ⟶ x1.
Assume H2: SNoLe 0 (minus_SNo x0) ⟶ not (SNoLt (minus_SNo x0) 0) ⟶ minus_SNo x0 ∈ omega ⟶ x1.
Apply nat_inv with x0, x1 leaving 3 subgoals.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Assume H3: x0 = 0.
Apply H2 leaving 3 subgoals.
Apply H3 with λ x2 x3 . SNoLe 0 (minus_SNo x3).
Apply minus_SNo_0 with λ x2 x3 . SNoLe 0 x3.
The subproof is completed by applying SNoLe_ref with 0.
Apply H3 with λ x2 x3 . not (SNoLt (minus_SNo x3) 0).
Apply minus_SNo_0 with λ x2 x3 . not (SNoLt x3 0).
The subproof is completed by applying SNoLt_irref with 0.
Apply H3 with λ x2 x3 . minus_SNo x3 ∈ omega.
Apply minus_SNo_0 with λ x2 x3 . x3 ∈ omega.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
Assume H3: ∃ x2 . and (nat_p x2) (x0 = ordsucc x2).
Apply H3 with x1.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (nat_p x3) (x0 = ordsucc x3)) x2.
Apply H4 with x1.
Assume H5: nat_p x2.
Assume H6: x0 = ordsucc x2.
Apply H1 leaving 2 subgoals.
Apply minus_SNo_0 with λ x3 x4 . SNoLt (minus_SNo x0) x3.
Apply minus_SNo_Lt_contra with 0, x0 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
Apply omega_SNo with x0.
The subproof is completed by applying H0.
Apply ordinal_In_SNoLt with x0, 0 leaving 2 subgoals.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply H6 with λ x3 x4 . 0 ∈ x4.
Apply nat_0_in_ordsucc with x2.
The subproof is completed by applying H5.
Apply minus_SNo_invol with x0, λ x3 x4 . x4 ∈ omega leaving 2 subgoals.
Apply omega_SNo with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
■