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.
Assume H0: SNo x0.
Assume H1: SNo x1.
Assume H2: SNo x2.
Claim L3: SNo (minus_SNo x1)
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H1.
Claim L4: SNo (minus_SNo x2)
Apply SNo_minus_SNo with x2.
The subproof is completed by applying H2.
Claim L5: add_SNo x0 (minus_SNo x2) = add_SNo (add_SNo x0 (minus_SNo x1)) (add_SNo x1 (minus_SNo x2))
Apply add_SNo_assoc with x0, minus_SNo x1, add_SNo x1 (minus_SNo x2), λ x3 x4 . add_SNo x0 (minus_SNo x2) = x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply SNo_add_SNo with x1, minus_SNo x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
set y3 to be add_SNo x0 (minus_SNo x2)
set y4 to be add_SNo x1 (add_SNo (minus_SNo x2) (add_SNo x2 (minus_SNo y3)))
Claim L5: ∀ x5 : ι → ο . x5 y4x5 y3
Let x5 of type ιο be given.
Assume H5: x5 (add_SNo x2 (add_SNo (minus_SNo y3) (add_SNo y3 (minus_SNo y4)))).
set y6 to be λ x6 . x5
set y7 to be λ x7 x8 . y6 (add_SNo x2 x7) (add_SNo x2 x8)
Apply add_SNo_minus_L2 with y3, minus_SNo y4, λ x8 x9 . y7 x9 x8 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
The subproof is completed by applying H5.
Let x5 of type ιιο be given.
Apply L5 with λ x6 . x5 x6 y4x5 y4 x6.
Assume H6: x5 y4 y4.
The subproof is completed by applying H6.
Apply L5 with λ x3 x4 . SNoLe (abs_SNo x4) (add_SNo (abs_SNo (add_SNo x0 (minus_SNo x1))) (abs_SNo (add_SNo x1 (minus_SNo x2)))).
Apply SNo_triangle with add_SNo x0 (minus_SNo x1), add_SNo x1 (minus_SNo x2) leaving 2 subgoals.
Apply SNo_add_SNo with x0, minus_SNo x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply SNo_add_SNo with x1, minus_SNo x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.