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.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: ∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x6 x1) (mul_SNo x0 x7)) (add_SNo x2 (mul_SNo x6 x7)).
Assume H4: SNo x3.
Assume H5: SNoLt x2 x3.
Assume H6: x4 ∈ SNoL x0.
Assume H7: x5 ∈ SNoL x1.
Assume H8: SNoLe (add_SNo x3 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)).
Assume H9: SNo x5.
Assume H10: SNo (mul_SNo x4 x5).
Assume H11: SNoLt (add_SNo x3 (mul_SNo x4 x5)) (add_SNo x2 (mul_SNo x4 x5)).
Apply FalseE with SNoLt (mul_SNo x0 x1) x3.
Apply SNoLt_irref with add_SNo x2 (mul_SNo x4 x5).
Claim L12: SNo (add_SNo x2 (mul_SNo x4 x5))
Apply SNo_add_SNo with x2, mul_SNo x4 x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H10.
Claim L13: SNo (add_SNo x3 (mul_SNo x4 x5))
Apply SNo_add_SNo with x3, mul_SNo x4 x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H10.
Apply SNoLt_tra with add_SNo x2 (mul_SNo x4 x5), add_SNo x3 (mul_SNo x4 x5), add_SNo x2 (mul_SNo x4 x5) leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
The subproof is completed by applying L12.
Apply add_SNo_Lt1 with x2, mul_SNo x4 x5, x3 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H10.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H11.
■