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: SNoLt x2 x0.
Assume H5: SNoLt x3 x1.
Apply mul_SNo_prop_1 with x0, x1, SNoLt (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H6: SNo (mul_SNo x0 x1).
Assume H7: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo (mul_SNo x0 x1) (mul_SNo x4 x5)).
Assume H8: ∀ x4 . x4 ∈ SNoR x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo (mul_SNo x0 x1) (mul_SNo x4 x5)).
Assume H9: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)).
Assume H10: ∀ x4 . x4 ∈ SNoR x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x0 x1) (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)).
Apply mul_SNo_prop_1 with x2, x1, SNoLt (add_SNo (mul_SNo x2 x1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 x1) (mul_SNo x2 x3)) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Assume H11: SNo (mul_SNo x2 x1).
Assume H12: ∀ x4 . x4 ∈ SNoL x2 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x4 x1) (mul_SNo x2 x5)) (add_SNo (mul_SNo x2 x1) (mul_SNo x4 x5)).
Assume H13: ∀ x4 . x4 ∈ SNoR x2 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x4 x1) (mul_SNo x2 x5)) (add_SNo (mul_SNo x2 x1) (mul_SNo x4 x5)).
Assume H14: ∀ x4 . x4 ∈ SNoL x2 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ SNoLt (add_SNo (mul_SNo x2 x1) (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x2 x5)).
Assume H15: ∀ x4 . ... ⟶ ∀ x5 . ... ⟶ SNoLt (add_SNo (mul_SNo x2 x1) (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x2 x5)).
...
■