Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ∀ x2 . x2 ∈ SNoL x0 ⟶ ∀ x3 . x3 ∈ SNoL 1 ⟶ SNoLt (add_SNo (mul_SNo x2 1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 1) (mul_SNo x2 x3)).
Assume H1: 0 ∈ SNoL 1.
Assume H2: x1 ∈ SNoL x0.
Assume H3: SNo x1.
Assume H4: add_SNo (mul_SNo x1 1) (mul_SNo x0 0) = x1.
Assume H5: add_SNo (mul_SNo x0 1) (mul_SNo x1 0) = mul_SNo x0 1.
Apply H4 with λ x2 x3 . SNoLt x2 (mul_SNo x0 1).
Apply H5 with λ x2 x3 . SNoLt (add_SNo (mul_SNo x1 1) (mul_SNo x0 0)) x2.
Apply H0 with x1, 0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
■