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 (mul_SNo x0 x1)
Apply SNo_mul_SNo with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply SNo_max_ordinal with mul_SNo x0 x1 leaving 2 subgoals.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Assume H5: x2 ∈ SNoS_ (SNoLev (mul_SNo x0 x1)).
Apply SNoS_E2 with SNoLev (mul_SNo x0 x1), x2, SNoLt x2 (mul_SNo x0 x1) leaving 3 subgoals.
Apply SNoLev_ordinal with mul_SNo x0 x1.
The subproof is completed by applying L4.
The subproof is completed by applying H5.
Assume H6: SNoLev x2 ∈ SNoLev (mul_SNo x0 x1).
Assume H7: ordinal (SNoLev x2).
Assume H8: SNo x2.
Assume H9: SNo_ (SNoLev x2) x2.
Apply SNoLt_trichotomy_or_impred with x2, mul_SNo x0 x1, SNoLt x2 (mul_SNo x0 x1) leaving 5 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying L4.
Assume H10: SNoLt x2 (mul_SNo x0 x1).
The subproof is completed by applying H10.
Assume H10: x2 = mul_SNo x0 x1.
Apply FalseE with SNoLt x2 (mul_SNo x0 x1).
Apply In_irref with SNoLev x2.
Apply H10 with λ x3 x4 . SNoLev x2 ∈ SNoLev x4.
The subproof is completed by applying H6.
Assume H10: SNoLt (mul_SNo x0 x1) x2.
Apply FalseE with SNoLt x2 (mul_SNo x0 x1).
Apply mul_SNo_SNoR_interpolate_impred with x0, x1, x2, False leaving 5 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply SNoR_I with mul_SNo x0 x1, x2 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H8.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Let x3 of type ι be given.
Assume H11: x3 ∈ SNoL x0.
Let x4 of type ι be given.
Assume H12: x4 ∈ SNoR x1.
Apply FalseE with SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4)) ⟶ False.
Apply SNoR_E with x1, x4, False leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H12.
Assume H13: SNo x4.
Apply ordinal_SNoLev with x1, λ x5 x6 . SNoLev x4 ∈ x6 ⟶ SNoLt x1 x4 ⟶ False leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H14: SNoLev x4 ∈ x1.
Assume H15: SNoLt x1 x4.
Apply SNoLt_irref with x1.
Apply SNoLt_tra with x1, x4, x1 leaving 5 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H13.
The subproof is completed by applying L3.
The subproof is completed by applying H15.
Apply ordinal_SNoLev_max with x1, x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Let x3 of type ι be given.
Assume H11: x3 ∈ SNoR x0.
Apply FalseE with ∀ x4 . x4 ∈ SNoL x1 ⟶ SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4)) ⟶ False.
Apply SNoR_E with x0, x3, False leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H11.
Assume H12: SNo x3.
Apply ordinal_SNoLev with x0, λ x4 x5 . SNoLev x3 ∈ x5 ⟶ SNoLt x0 x3 ⟶ False leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H13: SNoLev x3 ∈ x0.
Assume H14: SNoLt x0 x3.
Apply SNoLt_irref with x0.
Apply SNoLt_tra with x0, x3, x0 leaving 5 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H12.
The subproof is completed by applying L2.
The subproof is completed by applying H14.
Apply ordinal_SNoLev_max with x0, x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
■