Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_complete_ind with λ x0 . ∀ x1 . SNo x1 ⟶ SNoLev x1 = x0 ⟶ diadic_rational_p x1.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . SNo x2 ⟶ SNoLev x2 = x1 ⟶ diadic_rational_p x2.
Let x1 of type ι be given.
Assume H2: SNo x1.
Assume H3: SNoLev x1 = x0.
Apply dneg with diadic_rational_p x1.
Assume H4: not (diadic_rational_p x1).
Claim L5: ...
...
Apply SNoS_omega_SNoL_max_exists with x1, ∃ x2 . SNo_max_of (SNoL x1) x2, False leaving 4 subgoals.
The subproof is completed by applying L5.
Assume H6: SNoL x1 = 0.
Apply FalseE with ∃ x2 . SNo_max_of (SNoL x1) x2.
Apply H4.
Apply minus_SNo_invol with x1, λ x2 x3 . diadic_rational_p x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply minus_SNo_diadic_rational_p with minus_SNo x1.
Apply H3 with λ x2 x3 . minus_SNo x1 = x2, λ x2 x3 . diadic_rational_p x3 leaving 2 subgoals.
Let x2 of type ι → ι → ο be given.
Apply minus_SNo_Lev with x1, λ x3 x4 . x3 = minus_SNo x1, λ x3 x4 . x2 x4 x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply ordinal_SNoLev with minus_SNo x1.
Apply SNo_max_ordinal with minus_SNo x1 leaving 2 subgoals.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Apply minus_SNo_Lev with x1, λ x4 x5 . x3 ∈ SNoS_ x5 ⟶ SNoLt x3 (minus_SNo x1) leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H7: x3 ∈ SNoS_ (SNoLev x1).
Apply SNoS_E2 with SNoLev x1, x3, SNoLt x3 (minus_SNo x1) leaving 3 subgoals.
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H2.
The subproof is completed by applying H7.
Assume H8: SNoLev x3 ∈ SNoLev x1.
Assume H9: ordinal (SNoLev x3).
Assume H10: SNo x3.
Assume H11: SNo_ (SNoLev x3) x3.
Apply SNoLt_trichotomy_or_impred with x3, minus_SNo x1, SNoLt x3 (minus_SNo x1) leaving 5 subgoals.
The subproof is completed by applying H10.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H2.
Assume H12: SNoLt x3 (minus_SNo x1).
The subproof is completed by applying H12.
Assume H12: x3 = minus_SNo x1.
Apply FalseE with SNoLt x3 (minus_SNo x1).
Apply In_irref with SNoLev x3.
Apply H12 with λ x4 x5 . SNoLev x3 ∈ SNoLev x5.
Apply minus_SNo_Lev with x1, λ x4 x5 . SNoLev x3 ∈ x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H8.
Assume H12: SNoLt (minus_SNo x1) x3.
Apply FalseE with SNoLt x3 (minus_SNo x1).
Apply EmptyE with minus_SNo x3.
Apply H6 with λ x4 x5 . minus_SNo x3 ∈ x4.
Apply SNoL_I with x1, minus_SNo x3 leaving 4 subgoals.
The subproof is completed by applying H2.
Apply SNo_minus_SNo with x3.
The subproof is completed by applying H10.
Apply minus_SNo_Lev with x3, λ x4 x5 . x5 ∈ SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H8.
Apply minus_SNo_Lt_contra1 with x1, x3 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H10.
The subproof is completed by applying H12.
Apply omega_diadic_rational_p with x0.
Apply nat_p_omega with x0.
The subproof is completed by applying H0.
Assume H6: ∃ x2 . SNo_max_of (SNoL x1) x2.
The subproof is completed by applying H6.
Let x2 of type ι be given.
Assume H6: SNo_max_of (SNoL x1) x2.
Apply H6 with False.
Assume H7: and (x2 ∈ SNoL x1) (SNo x2).
Apply H7 with (∀ x3 . x3 ∈ SNoL x1 ⟶ SNo x3 ⟶ SNoLe x3 x2) ⟶ False.
Assume H8: x2 ∈ SNoL x1.
Assume H9: SNo x2.
Assume H10: ∀ x3 . x3 ∈ SNoL x1 ⟶ SNo x3 ⟶ SNoLe x3 x2.
Apply SNoL_E with x1, x2, False leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H8.
Assume H11: SNo x2.
Assume H12: SNoLev x2 ∈ SNoLev x1.
Assume H13: SNoLt x2 ....
...
■