Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0SNoS_ omega.
Let x1 of type ι be given.
Assume H1: x1SNoS_ omega.
Apply SNoS_E2 with omega, x0, add_SNo x0 x1SNoS_ omega leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H0.
Assume H2: SNoLev x0omega.
Assume H3: ordinal (SNoLev x0).
Assume H4: SNo x0.
Assume H5: SNo_ (SNoLev x0) x0.
Apply SNoS_E2 with omega, x1, add_SNo x0 x1SNoS_ omega leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H1.
Assume H6: SNoLev x1omega.
Assume H7: ordinal (SNoLev x1).
Assume H8: SNo x1.
Assume H9: SNo_ (SNoLev x1) x1.
Apply SNoS_I with omega, add_SNo x0 x1, SNoLev (add_SNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Claim L10: ordinal (SNoLev (add_SNo x0 x1))
Apply SNoLev_ordinal with add_SNo x0 x1.
Apply SNo_add_SNo with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply ordinal_In_Or_Subq with SNoLev (add_SNo x0 x1), omega, SNoLev (add_SNo x0 x1)omega leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying omega_ordinal.
Assume H11: SNoLev (add_SNo x0 x1)omega.
The subproof is completed by applying H11.
Assume H11: omegaSNoLev (add_SNo x0 x1).
Apply In_irref with add_SNo (SNoLev x0) (SNoLev x1), SNoLev (add_SNo x0 x1)omega.
Apply add_SNo_Lev_bd with x0, x1, add_SNo (SNoLev x0) (SNoLev x1) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply H11 with add_SNo (SNoLev x0) (SNoLev x1).
Apply add_SNo_In_omega with SNoLev x0, SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply SNoLev_ with add_SNo x0 x1.
Apply SNo_add_SNo with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.