Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ιο be given.
Let x3 of type ιο be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Apply SNoLev_PSNo with x0, x2, λ x4 x5 . PNoLt x5 (λ x6 . x6PSNo x0 x2) (SNoLev (PSNo x1 x3)) (λ x6 . x6PSNo x1 x3)PNoLt x0 x2 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoLev_PSNo with x1, x3, λ x4 x5 . PNoLt x0 (λ x6 . x6PSNo x0 x2) x5 (λ x6 . x6PSNo x1 x3)PNoLt x0 x2 x1 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: PNoLt x0 (λ x4 . x4PSNo x0 x2) x1 (λ x4 . x4PSNo x1 x3).
Apply PNoEqLt_tra with x0, x1, x2, λ x4 . x4PSNo x0 x2, x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply PNoEq_sym_ with x0, λ x4 . x4PSNo x0 x2, x2.
Apply PNoEq_PSNo with x0, x2.
The subproof is completed by applying H0.
Apply PNoLtEq_tra with x0, x1, λ x4 . x4PSNo x0 x2, λ x4 . x4PSNo x1 x3, x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply PNoEq_PSNo with x1, x3.
The subproof is completed by applying H1.