Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind with λ x0 . SNoLt 0 x0and (SNo (recip_SNo_pos x0)) (mul_SNo x0 (recip_SNo_pos x0) = 1).
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1SNoS_ (SNoLev x0)SNoLt 0 x1and (SNo (recip_SNo_pos x1)) (mul_SNo x1 (recip_SNo_pos x1) = 1).
Assume H2: SNoLt 0 x0.
Apply recip_SNo_pos_eq with x0, λ x1 x2 . and (SNo x2) (mul_SNo x0 x2 = 1) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNo_recipaux_lem2 with x0, recip_SNo_pos, and (SNo ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 1))) x0 recip_SNo_pos)) (mul_SNo x0 ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 1))) x0 recip_SNo_pos) = 1) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Assume H3: and (∀ x1 . x1famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 0)SNo x1) (∀ x1 . x1famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 1)SNo x1).
Apply H3 with (∀ x1 . x1famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 0)∀ x2 . x2famunion omega (λ x3 . ap (SNo_recipaux x0 recip_SNo_pos x3) 1)SNoLt x1 x2)and (SNo ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 1))) x0 recip_SNo_pos)) (mul_SNo x0 ((λ x1 . λ x2 : ι → ι . SNoCut (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 0)) (famunion omega (λ x3 . ap (SNo_recipaux x1 x2 x3) 1))) x0 recip_SNo_pos) = 1).
Assume H4: ∀ x1 . x1famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 0)SNo x1.
Assume H5: ∀ x1 . x1famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 1)SNo x1.
Assume H6: ∀ x1 . ...∀ x2 . x2famunion omega (λ x3 . ap (SNo_recipaux x0 recip_SNo_pos x3) 1)SNoLt x1 x2.
...