Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Assume H1: ordinal x1.
Claim L2: SNo x0
Apply ordinal_SNo with x0.
The subproof is completed by applying H0.
Claim L3: SNo x1
Apply ordinal_SNo with x1.
The subproof is completed by applying H1.
Claim L4: SNo x0
Apply ordinal_SNo with x0.
The subproof is completed by applying H0.
Claim L5: ordinal (ordsucc x1)
Apply ordinal_ordsucc with x1.
The subproof is completed by applying H1.
Claim L6: SNo (ordsucc x1)
Apply ordinal_SNo with ordsucc x1.
The subproof is completed by applying L5.
Apply add_SNo_com with x0, ordsucc x1, λ x2 x3 . x3 = ordsucc (add_SNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
Apply add_SNo_ordinal_SL with x1, x0, λ x2 x3 . x3 = ordsucc (add_SNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply add_SNo_com with x1, x0, λ x2 x3 . ordsucc x3 = ordsucc (add_SNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Let x2 of type ιιο be given.
Assume H7: x2 (ordsucc (add_SNo x0 x1)) (ordsucc (add_SNo x0 x1)).
The subproof is completed by applying H7.