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.
Apply minus_add_SNo_distr_m with x0, minus_SNo x1, λ x2 x3 . x3 = add_SNo x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H1.
set y2 to be add_SNo x0 (minus_SNo (minus_SNo x1))
set y3 to be add_SNo x1 y2
Claim L2: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2
Let x4 of type ι → ο be given.
Assume H2: x4 (add_SNo y2 y3).
set y5 to be λ x5 . x4
Apply minus_SNo_invol with y3, λ x6 x7 . y5 (add_SNo y2 x6) (add_SNo y2 x7) leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x4 of type ι → ι → ο be given.
Apply L2 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H3: x4 y3 y3.
The subproof is completed by applying H3.
■