Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLe 0 x0.
Assume H2: ∀ 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).
Apply nat_ind with λ x1 . and (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0)) (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2))) leaving 2 subgoals.
Apply SNo_sqrtaux_0 with x0, sqrt_SNo_nonneg, λ x1 x2 . and (∀ x3 . x3ap x2 0and (and (SNo x3) (SNoLe 0 x3)) (SNoLt (mul_SNo x3 x3) x0)) (∀ x3 . x3ap x2 1and (and (SNo x3) (SNoLe 0 x3)) (SNoLt x0 (mul_SNo x3 x3))).
Apply andI with ∀ x1 . x1ap (lam 2 (λ x2 . If_i (x2 = 0) (prim5 (SNoL_nonneg x0) sqrt_SNo_nonneg) (prim5 (SNoR x0) sqrt_SNo_nonneg))) 0and (and (SNo x1) (SNoLe 0 x1)) (SNoLt (mul_SNo x1 x1) x0), ∀ x1 . x1ap (lam 2 (λ x2 . If_i (x2 = 0) (prim5 (SNoL_nonneg x0) sqrt_SNo_nonneg) (prim5 (SNoR x0) sqrt_SNo_nonneg))) 1and (and (SNo x1) (SNoLe 0 x1)) (SNoLt x0 (mul_SNo x1 x1)) leaving 2 subgoals.
Let x1 of type ι be given.
Apply tuple_2_0_eq with prim5 (SNoL_nonneg x0) sqrt_SNo_nonneg, prim5 (SNoR x0) sqrt_SNo_nonneg, λ x2 x3 . x1x3and (and (SNo x1) (SNoLe 0 x1)) (SNoLt (mul_SNo x1 x1) x0).
Assume H3: x1{sqrt_SNo_nonneg x2|x2 ∈ SNoL_nonneg x0}.
Apply ReplE_impred with SNoL_nonneg x0, sqrt_SNo_nonneg, x1, and (and (SNo x1) (SNoLe 0 x1)) (SNoLt (mul_SNo x1 x1) x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2SNoL_nonneg x0.
Assume H5: x1 = sqrt_SNo_nonneg x2.
Apply SepE with SNoL x0, λ x3 . SNoLe 0 x3, x2, and (and (SNo x1) (SNoLe 0 x1)) (SNoLt (mul_SNo x1 x1) x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H6: x2SNoL x0.
Assume H7: SNoLe 0 ....
...
...
...