Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 x1 x2 . x2 ∈ SNoLev x0 ⟶ SNo x1 ⟶ SNoLev x1 = x2 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ and (and (SNo x1) (SNoLev x1 ∈ SNoLev x0)) (SNoLt x0 x1).
Claim L1: 0 ∈ 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 L2: SNo 0
The subproof is completed by applying SNo_0.
Claim L3: SNoLev 0 = 0
The subproof is completed by applying SNoLev_0.
Claim L4: 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 L5: not (SNoLev 0 ∈ SNoLev 1 ⟶ and (and (SNo 0) (SNoLev 0 ∈ SNoLev 1)) (SNoLt 1 0))
Assume H5: SNoLev 0 ∈ SNoLev 1 ⟶ and (and (SNo 0) (SNoLev 0 ∈ SNoLev 1)) (SNoLt 1 0).
Apply H5 with False leaving 2 subgoals.
The subproof is completed by applying L4.
Assume H6: and (SNo 0) (SNoLev 0 ∈ SNoLev 1).
Assume H7: SNoLt 1 0.
Apply SNoLt_irref with 0.
Apply SNoLt_tra with 0, 1, 0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
The subproof is completed by applying SNoLt_0_1.
The subproof is completed by applying H7.
Apply L5.
Apply H0 with 1, 0, 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■