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: ∀ x3 x4 . SNoCutP x3 x4 ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 : ο . (∀ x7 . x7 ∈ SNoL x0 ⟶ ∀ x8 . x8 ∈ SNoL x1 ⟶ x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ (∀ x7 . x7 ∈ SNoR x0 ⟶ ∀ x8 . x8 ∈ SNoR x1 ⟶ x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . x5 ∈ SNoL x0 ⟶ ∀ x6 . x6 ∈ SNoL x1 ⟶ add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6))) ∈ x3) ⟶ (∀ x5 . x5 ∈ SNoR x0 ⟶ ∀ x6 . x6 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6))) ∈ x3) ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 : ο . (∀ x7 . x7 ∈ SNoL x0 ⟶ ∀ x8 . x8 ∈ SNoR x1 ⟶ x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ (∀ x7 . x7 ∈ SNoR x0 ⟶ ∀ x8 . x8 ∈ SNoL x1 ⟶ x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . x5 ∈ SNoL x0 ⟶ ∀ x6 . x6 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6))) ∈ x4) ⟶ (∀ x5 . x5 ∈ SNoR x0 ⟶ ∀ x6 . x6 ∈ SNoL x1 ⟶ add_SNo (mul_SNo x5 x1) (add_SNo (mul_SNo x0 x6) (minus_SNo (mul_SNo x5 x6))) ∈ x4) ⟶ mul_SNo x0 x1 = SNoCut x3 x4 ⟶ x2.
Apply mul_SNo_eq_2 with x0, x1, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H3: ∀ x5 . ... ⟶ ∀ x6 : ο . (∀ x7 . ... ⟶ ∀ x8 . ... ⟶ x5 = add_SNo (mul_SNo x7 ...) ... ⟶ x6) ⟶ (∀ x7 . x7 ∈ SNoR x0 ⟶ ∀ x8 . x8 ∈ SNoR x1 ⟶ x5 = add_SNo (mul_SNo x7 x1) (add_SNo (mul_SNo x0 x8) (minus_SNo (mul_SNo x7 x8))) ⟶ x6) ⟶ x6.
...
■