Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιο be given.
Assume H0: ∀ x1 x2 . SNoCutP x1 x2(∀ x3 . x3x1x0 x3)(∀ x3 . x3x2x0 x3)x0 (SNoCut x1 x2).
Claim L1: ∀ x1 . ordinal x1∀ x2 . SNo x2SNoLev x2x1x0 x2
Apply ordinal_ind with λ x1 . ∀ x2 . SNo x2SNoLev x2x1x0 x2.
Let x1 of type ι be given.
Assume H1: ordinal x1.
Assume H2: ∀ x2 . x2x1∀ x3 . SNo x3SNoLev x3x2x0 x3.
Let x2 of type ι be given.
Assume H3: SNo x2.
Assume H4: SNoLev x2x1.
Claim L5: ordinal (SNoLev x2)
Apply SNoLev_ordinal with x2.
The subproof is completed by applying H3.
Apply SNo_etaE with x2, x0 x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H6: SNoCutP x3 x4.
Assume H7: ∀ x5 . x5x3SNoLev x5SNoLev x2.
Assume H8: ∀ x5 . x5x4SNoLev x5SNoLev x2.
Assume H9: x2 = SNoCut x3 x4.
Apply H6 with x0 x2.
Assume H10: and (∀ x5 . x5x3SNo x5) (∀ x5 . x5x4SNo x5).
Apply H10 with (∀ x5 . x5x3∀ x6 . x6x4SNoLt x5 x6)x0 x2.
Assume H11: ∀ x5 . x5x3SNo x5.
Assume H12: ∀ x5 . x5x4SNo x5.
Assume H13: ∀ x5 . x5x3∀ x6 . x6x4SNoLt x5 x6.
Apply H9 with λ x5 x6 . x0 x6.
Apply H0 with x3, x4 leaving 3 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H14: x5x3.
Apply H2 with SNoLev x2, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H11 with x5.
The subproof is completed by applying H14.
Apply H7 with x5.
The subproof is completed by applying H14.
Let x5 of type ι be given.
Assume H14: x5x4.
Apply H2 with SNoLev x2, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply H12 with x5.
The subproof is completed by applying H14.
Apply H8 with x5.
The subproof is completed by applying H14.
Let x1 of type ι be given.
Assume H2: SNo x1.
Claim L3: ordinal (ordsucc (SNoLev x1))
Apply ordinal_ordsucc with SNoLev x1.
Apply SNoLev_ordinal with x1.
The subproof is completed by applying H2.
Apply L1 with ordsucc (SNoLev x1), x1 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H2.
The subproof is completed by applying ordsuccI2 with SNoLev x1.