Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNoLe 0 x0.
Assume H2: 0SNoLev x0.
Apply sqrt_SNo_nonneg_0 with λ x1 x2 . x1(λ x3 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x3) 0) 0.
Apply SNo_sqrtaux_0 with x0, sqrt_SNo_nonneg, λ x1 x2 . sqrt_SNo_nonneg 0ap x2 0.
Apply tuple_2_0_eq with prim5 (SNoL_nonneg x0) sqrt_SNo_nonneg, prim5 (SNoR x0) sqrt_SNo_nonneg, λ x1 x2 . sqrt_SNo_nonneg 0x2.
Apply ReplI with SNoL_nonneg x0, sqrt_SNo_nonneg, 0.
Apply SepI with SNoL x0, λ x1 . SNoLe 0 x1, 0 leaving 2 subgoals.
Apply SNoL_I with x0, 0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with λ x1 x2 . x2SNoLev x0.
The subproof is completed by applying H2.
Apply SNoLeE with 0, x0, SNoLt 0 x0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H3: SNoLt 0 x0.
The subproof is completed by applying H3.
Assume H3: 0 = x0.
Apply FalseE with SNoLt 0 x0.
Apply EmptyE with 0.
Apply SNoLev_0 with λ x1 x2 . 0x1.
Apply H3 with λ x1 x2 . 0SNoLev x2.
The subproof is completed by applying H2.
The subproof is completed by applying SNoLe_ref with 0.