Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLe 0 x0.
Assume H2: 1 ∈ SNoLev x0.
Assume H3: famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) x1) = 0.
Apply SNoLt_trichotomy_or_impred with x0, 1, False leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Assume H4: SNoLt x0 1.
Apply EmptyE with sqrt_SNo_nonneg 1.
Apply H3 with λ x1 x2 . sqrt_SNo_nonneg 1 ∈ x1.
Apply famunionI with omega, λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1, 0, sqrt_SNo_nonneg 1 leaving 2 subgoals.
Apply nat_p_omega with 0.
The subproof is completed by applying nat_0.
Apply SNo_sqrtaux_0 with x0, sqrt_SNo_nonneg, λ x1 x2 . sqrt_SNo_nonneg 1 ∈ ap x2 1.
Apply tuple_2_1_eq with prim5 (SNoL_nonneg x0) sqrt_SNo_nonneg, prim5 (SNoR x0) sqrt_SNo_nonneg, λ x1 x2 . sqrt_SNo_nonneg 1 ∈ x2.
Apply ReplI with SNoR x0, sqrt_SNo_nonneg, 1.
Apply SNoR_I with x0, 1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply ordinal_SNoLev with 1, λ x1 x2 . x2 ∈ SNoLev x0 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Assume H4: x0 = 1.
Apply In_irref with 1.
Apply ordinal_SNoLev with 1, λ x1 x2 . 1 ∈ x1 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
Apply H4 with λ x1 x2 . 1 ∈ SNoLev x1.
The subproof is completed by applying H2.
Assume H4: SNoLt 1 x0.
Apply EmptyE with div_SNo (add_SNo x0 (mul_SNo 1 0)) (add_SNo 1 0).
Apply H3 with λ x1 x2 . div_SNo (add_SNo x0 (mul_SNo 1 0)) (add_SNo 1 0) ∈ x1.
Apply famunionI with omega, λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1, 1, div_SNo (add_SNo x0 (mul_SNo 1 0)) (add_SNo 1 0) leaving 2 subgoals.
Apply nat_p_omega with 1.
The subproof is completed by applying nat_1.
Apply SNo_sqrtaux_S with x0, sqrt_SNo_nonneg, 0, λ x1 x2 . div_SNo (add_SNo x0 (mul_SNo 1 0)) (add_SNo 1 0) ∈ ap x2 1 leaving 2 subgoals.
The subproof is completed by applying nat_0.
Apply tuple_2_1_eq with binunion (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0) (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 1) x0), binunion (binunion (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 1) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0) (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0) x0)) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 1) (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 1) x0), λ x1 x2 . div_SNo (add_SNo x0 (mul_SNo 1 0)) (add_SNo 1 0) ∈ x2.
Apply binunionI1 with binunion (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 1) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0) (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0) x0), SNo_sqrtauxset (ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 1) (ap (SNo_sqrtaux ... ... 0) 1) ..., ....
...
■