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: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Assume H3: SNo x3.
Assume H4: SNoLe x2 x0.
Assume H5: SNoLe x3 x1.
Apply SNoLeE with x2, x0, SNoLe (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)) leaving 5 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H6: SNoLt x2 x0.
Apply SNoLeE with x3, x1, SNoLe (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)) leaving 5 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Assume H7: SNoLt x3 x1.
Apply SNoLtLe with add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3), add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3).
Apply mul_SNo_Lt with x0, x1, x2, x3 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Assume H7: x3 = x1.
Apply H7 with λ x4 x5 . SNoLe (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x5)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x5)).
Apply add_SNo_com with mul_SNo x2 x1, mul_SNo x0 x1, λ x4 x5 . SNoLe x5 (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x1)) leaving 3 subgoals.
Apply SNo_mul_SNo with x2, x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply SNo_mul_SNo with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying SNoLe_ref with add_SNo (mul_SNo x0 x1) (mul_SNo x2 x1).
Assume H6: x2 = x0.
Apply H6 with λ x4 x5 . SNoLe (add_SNo (mul_SNo x5 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x5 x3)).
The subproof is completed by applying SNoLe_ref with add_SNo (mul_SNo x0 x1) (mul_SNo x0 x3).