Search for blocks/addresses/...

Proofgold Proof

pf
Apply sqrt_SNo_nonneg_eq with 0, λ x0 x1 . x1 = 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Claim L0: ∀ x0 . nat_p x0 ⟶ and ((λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 0) x0 = 0) ((λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 1) x0 = 0)
Apply nat_ind with λ x0 . and ((λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 0) x0 = 0) ((λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 1) x0 = 0) leaving 2 subgoals.
Apply andI with (λ x0 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x0) 0) 0 = 0, (λ x0 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x0) 1) 0 = 0 leaving 2 subgoals.
Apply SNo_sqrtaux_0 with 0, sqrt_SNo_nonneg, λ x0 x1 . ap x1 0 = 0.
Apply tuple_2_0_eq with prim5 (SNoL_nonneg 0) sqrt_SNo_nonneg, prim5 (SNoR 0) sqrt_SNo_nonneg, λ x0 x1 . ... = 0.
...
...
...
Apply Empty_eq with famunion omega (λ x0 . (λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 0) x0), λ x0 x1 . SNoCut x1 (famunion omega (λ x2 . (λ x3 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x3) 1) x2)) = 0 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H1: x0 ∈ famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x2) 0) x1).
Apply famunionE_impred with omega, λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 0, x0, False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H2: x1 ∈ omega.
Apply L0 with x1, x0 ∈ ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 0 ⟶ False leaving 2 subgoals.
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Assume H3: (λ x2 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x2) 0) x1 = 0.
Assume H4: ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 1 = 0.
Apply H3 with λ x2 x3 . nIn x0 x3.
The subproof is completed by applying EmptyE with x0.
Apply Empty_eq with famunion omega (λ x0 . (λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 1) x0), λ x0 x1 . SNoCut 0 x1 = 0 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H1: x0 ∈ famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x2) 1) x1).
Apply famunionE_impred with omega, λ x1 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 1, x0, False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H2: x1 ∈ omega.
Apply L0 with x1, x0 ∈ ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 1 ⟶ False leaving 2 subgoals.
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Assume H3: ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x1) 0 = 0.
Assume H4: (λ x2 . ap (SNo_sqrtaux 0 sqrt_SNo_nonneg x2) 1) x1 = 0.
Apply H4 with λ x2 x3 . nIn x0 x3.
The subproof is completed by applying EmptyE with x0.
The subproof is completed by applying SNoCut_0_0.
■