Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ SNoS_ omega.
Apply SNoS_E2 with omega, x0, SNoLe 0 x0 ⟶ sqrt_SNo_nonneg x0 ∈ real leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Assume H1: SNoLev x0 ∈ omega.
Assume H2: ordinal (SNoLev x0).
Assume H3: SNo x0.
Assume H4: SNo_ (SNoLev x0) x0.
Apply SNoLev_ind with λ x1 . SNoLev x1 ∈ omega ⟶ SNoLe 0 x1 ⟶ sqrt_SNo_nonneg x1 ∈ real, x0 leaving 3 subgoals.
Let x1 of type ι be given.
Assume H5: SNo x1.
Assume H6: ∀ x2 . x2 ∈ SNoS_ (SNoLev x1) ⟶ SNoLev x2 ∈ omega ⟶ SNoLe 0 x2 ⟶ sqrt_SNo_nonneg x2 ∈ real.
Assume H7: SNoLev x1 ∈ omega.
Assume H8: SNoLe 0 x1.
Claim L9: ...
...
Apply ordinal_In_Or_Subq with 0, SNoLev x1, sqrt_SNo_nonneg x1 ∈ real leaving 4 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H5.
Assume H10: 0 ∈ SNoLev x1.
Apply ordinal_In_Or_Subq with 1, SNoLev x1, sqrt_SNo_nonneg x1 ∈ real leaving 4 subgoals.
The subproof is completed by applying ordinal_1.
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H5.
Assume H11: 1 ∈ SNoLev x1.
Apply sqrt_SNo_nonneg_eq with x1, λ x2 x3 . x3 ∈ real leaving 2 subgoals.
The subproof is completed by applying H5.
Claim L12: ...
...
Claim L13: ...
...
Apply SNo_sqrt_SNo_SNoCutP with x1, SNoCut (famunion omega (λ x2 . (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 0) x2)) (famunion omega (λ x2 . (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 1) x2)) ∈ real leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
Assume H14: and (∀ x2 . x2 ∈ famunion omega (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 0) ⟶ SNo x2) (∀ x2 . x2 ∈ famunion omega (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 1) ⟶ SNo x2).
Apply H14 with (∀ x2 . x2 ∈ famunion omega (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 0) ⟶ ∀ x3 . x3 ∈ famunion omega (λ x4 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x4) 1) ⟶ SNoLt x2 x3) ⟶ SNoCut (famunion omega (λ x2 . (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 0) x2)) (famunion omega (λ x2 . (λ x3 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x3) 1) x2)) ∈ real.
Assume H15: ∀ x2 . x2 ∈ famunion omega (λ x3 . (λ x4 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x4) 0) x3) ⟶ SNo x2.
Assume H16: ∀ x2 . x2 ∈ famunion omega (λ x3 . (λ x4 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x4) 1) x3) ⟶ SNo x2.
Assume H17: ∀ x2 . x2 ∈ famunion ... ... ⟶ ∀ x3 . x3 ∈ famunion omega (λ x4 . (λ x5 . ap (SNo_sqrtaux x1 sqrt_SNo_nonneg x5) 1) x4) ⟶ SNoLt x2 x3.
...
...
...
...
...
■