Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind with λ x0 . SNoLe 0 x0and (and (SNo (sqrt_SNo_nonneg x0)) (SNoLe 0 (sqrt_SNo_nonneg x0))) (mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0).
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1SNoS_ (SNoLev x0)SNoLe 0 x1and (and (SNo (sqrt_SNo_nonneg x1)) (SNoLe 0 (sqrt_SNo_nonneg x1))) (mul_SNo (sqrt_SNo_nonneg x1) (sqrt_SNo_nonneg x1) = x1).
Assume H2: SNoLe 0 x0.
Apply sqrt_SNo_nonneg_eq with x0, λ x1 x2 . and (and (SNo x2) (SNoLe 0 x2)) (mul_SNo x2 x2 = x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Claim L3: ...
...
Apply sqrt_SNo_nonneg_prop1b with x0, and (and (SNo ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 1))) x0 sqrt_SNo_nonneg)) (SNoLe 0 ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 1))) x0 sqrt_SNo_nonneg))) (mul_SNo ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 1))) x0 sqrt_SNo_nonneg) ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 1))) x0 sqrt_SNo_nonneg) = x0) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply sqrt_SNo_nonneg_prop1a with x0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Assume H4: and (∀ x1 . x1famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0)SNo x1) (∀ x1 . x1famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1)SNo x1).
Apply H4 with ...and (and (SNo ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 1))) x0 sqrt_SNo_nonneg)) (SNoLe 0 ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_sqrtaux x1 x2 x3) 1))) x0 sqrt_SNo_nonneg))) (mul_SNo ((λ x1 . λ x2 : ι → ι . ...) ... ...) ... = ...).
...