Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ιιι) → ιι be given.
Assume H0: ∀ x1 . SNo x1∀ x2 x3 : ι → ι → ι . (∀ x4 . x4SNoS_ (SNoLev x1)x2 x4 = x3 x4)x0 x1 x2 = x0 x1 x3.
Let x1 of type ι be given.
Assume H1: SNo x1.
Claim L2: ∀ x2 . ∀ x3 x4 : ι → ι → ι → ι . ...(λ x5 . λ x6 : ι → ι → ι → ι . If_iii (ordinal x5) (λ x7 . If_ii (x7SNoS_ (ordsucc x5)) (x0 x7 (λ x8 . x6 (SNoLev x8) x8)) (Descr_ii (λ x8 : ι → ι . True))) (λ x7 . Descr_ii ...)) ... ... = ...
...
Apply In_rec_iii_eq with λ x2 . λ x3 : ι → ι → ι → ι . If_iii (ordinal x2) (λ x4 . If_ii (x4SNoS_ (ordsucc x2)) (x0 x4 (λ x5 . x3 (SNoLev x5) x5)) (Descr_ii (λ x5 : ι → ι . True))) (λ x4 . Descr_ii (λ x5 : ι → ι . True)), SNoLev x1, λ x2 x3 : ι → ι → ι . x3 x1 = x0 x1 (λ x4 . In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (ordinal x5) (λ x7 . If_ii (x7SNoS_ (ordsucc x5)) (x0 x7 (λ x8 . x6 (SNoLev x8) x8)) (Descr_ii (λ x8 : ι → ι . True))) (λ x7 . Descr_ii (λ x8 : ι → ι . True))) (SNoLev x4) x4) leaving 2 subgoals.
The subproof is completed by applying L2.
Claim L3: ordinal (SNoLev x1)
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H1.
Apply If_iii_1 with ordinal (SNoLev x1), λ x2 . If_ii (x2SNoS_ (ordsucc (SNoLev x1))) (x0 x2 (λ x3 . In_rec_iii (λ x4 . λ x5 : ι → ι → ι → ι . If_iii (ordinal x4) (λ x6 . If_ii (x6SNoS_ (ordsucc x4)) (x0 x6 (λ x7 . x5 (SNoLev x7) x7)) (Descr_ii (λ x7 : ι → ι . True))) (λ x6 . Descr_ii (λ x7 : ι → ι . True))) (SNoLev x3) x3)) (Descr_ii (λ x3 : ι → ι . True)), λ x2 . Descr_ii (λ x3 : ι → ι . True), λ x2 x3 : ι → ι → ι . x3 x1 = x0 x1 (λ x4 . In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (ordinal x5) (λ x7 . If_ii (x7SNoS_ (ordsucc x5)) (x0 x7 (λ x8 . x6 (SNoLev x8) x8)) (Descr_ii (λ x8 : ι → ι . True))) (λ x7 . Descr_ii (λ x8 : ι → ι . True))) (SNoLev x4) x4) leaving 2 subgoals.
The subproof is completed by applying L3.
Claim L4: x1SNoS_ (ordsucc (SNoLev x1))
Apply SNoS_SNoLev with x1.
The subproof is completed by applying H1.
Apply If_ii_1 with x1SNoS_ (ordsucc (SNoLev x1)), x0 x1 (λ x2 . In_rec_iii (λ x3 . λ x4 : ι → ι → ι → ι . If_iii (ordinal x3) (λ x5 . If_ii (x5SNoS_ (ordsucc x3)) (x0 x5 (λ x6 . x4 (SNoLev x6) x6)) (Descr_ii (λ x6 : ι → ι . True))) (λ x5 . Descr_ii (λ x6 : ι → ι . True))) (SNoLev x2) x2), Descr_ii (λ x2 : ι → ι . True).
The subproof is completed by applying L4.