Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 x1 x2 x3 . ordinal (SNoLev x0) ⟶ x2 = minus_SNo x3 ⟶ SNoLev x3 ∈ SNoLev x0 ⟶ SNoLev (minus_SNo x3) ⊆ SNoLev x3 ⟶ ordinal (SNoLev (minus_SNo x3)) ⟶ ordinal (ordsucc (SNoLev x2)) ⟶ x1 ∈ SNoLev x0.
Claim L1: ordinal (SNoLev 1)
Apply SNoLev_ordinal with 1.
The subproof is completed by applying SNo_1.
Claim L2: 0 = minus_SNo 0
Let x0 of type ι → ι → ο be given.
The subproof is completed by applying minus_SNo_0 with λ x1 x2 . x0 x2 x1.
Claim L3: SNoLev 0 ∈ SNoLev 1
Apply SNoLev_0 with λ x0 x1 . x1 ∈ SNoLev 1.
Apply ordinal_SNoLev with 1, λ x0 x1 . 0 ∈ x1 leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
The subproof is completed by applying In_0_1.
Claim L4: SNoLev (minus_SNo 0) ⊆ SNoLev 0
Apply minus_SNo_Lev with 0, λ x0 x1 . x1 ⊆ SNoLev 0 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with λ x0 x1 . x1 ⊆ x1.
The subproof is completed by applying Subq_ref with 0.
Claim L5: ordinal (SNoLev (minus_SNo 0))
Apply minus_SNo_Lev with 0, λ x0 x1 . ordinal x1 leaving 2 subgoals.
The subproof is completed by applying SNo_0.
Apply SNoLev_0 with λ x0 x1 . ordinal x1.
The subproof is completed by applying ordinal_Empty.
Claim L6: not (ordinal (ordsucc (SNoLev 0)) ⟶ 2 ∈ SNoLev 1)
Apply SNoLev_0 with λ x0 x1 . not (ordinal (ordsucc x1) ⟶ 2 ∈ SNoLev 1).
Apply ordinal_SNoLev with 1, λ x0 x1 . not (ordinal 1 ⟶ 2 ∈ x1) leaving 2 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
Assume H6: ordinal 1 ⟶ 2 ∈ 1.
Apply In_no2cycle with 1, 2 leaving 2 subgoals.
The subproof is completed by applying In_1_2.
Apply H6.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
Apply L6.
Apply H0 with 1, 2, 0, 0 leaving 5 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
■