Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: SNo x0.
Assume H1: SNo x1.
Let x2 of type ι be given.
Assume H2: x2 ∈ SNoL (mul_SNo x0 x1).
Let x3 of type ο be given.
Assume H3: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) ⟶ x3.
Assume H4: ∀ x4 . x4 ∈ SNoR x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) ⟶ x3.
Apply mul_SNo_SNoL_interpolate with x0, x1, x2, x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Assume H5: ∃ x4 . and (x4 ∈ SNoL x0) (∃ x5 . and (x5 ∈ SNoL x1) (SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)))).
Apply H5 with x3.
Let x4 of type ι be given.
Assume H6: (λ x5 . and (x5 ∈ SNoL x0) (∃ x6 . and (x6 ∈ SNoL x1) (SNoLe (add_SNo x2 (mul_SNo x5 x6)) (add_SNo (mul_SNo x5 x1) (mul_SNo x0 x6))))) x4.
Apply H6 with x3.
Assume H7: x4 ∈ SNoL x0.
Assume H8: ∃ x5 . and (x5 ∈ SNoL x1) (SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))).
Apply H8 with x3.
Let x5 of type ι be given.
Assume H9: (λ x6 . and (x6 ∈ SNoL x1) (SNoLe (add_SNo x2 (mul_SNo x4 x6)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x6)))) x5.
Apply H9 with x3.
Assume H10: x5 ∈ SNoL x1.
Assume H11: SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)).
Apply H3 with x4, x5 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Assume H5: ∃ x4 . and (x4 ∈ SNoR x0) (∃ x5 . and (x5 ∈ SNoR x1) (SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)))).
Apply H5 with x3.
Let x4 of type ι be given.
Assume H6: (λ x5 . and (x5 ∈ SNoR x0) (∃ x6 . and (x6 ∈ SNoR x1) (SNoLe (add_SNo x2 (mul_SNo x5 x6)) (add_SNo (mul_SNo x5 x1) (mul_SNo x0 x6))))) x4.
Apply H6 with x3.
Assume H7: x4 ∈ SNoR x0.
Assume H8: ∃ x5 . and (x5 ∈ SNoR x1) (SNoLe ... ...).
...
■