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.
Claim L2: SNo (minus_SNo x0)
Apply SNo_minus_SNo with x0.
The subproof is completed by applying H0.
Claim L3: SNo (minus_SNo x1)
Apply SNo_minus_SNo with x1.
The subproof is completed by applying H1.
Claim L4: SNo (add_SNo x0 x1)
Apply SNo_add_SNo with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Claim L5: add_SNo (add_SNo x0 x1) (minus_SNo (add_SNo x0 x1)) = add_SNo (add_SNo x0 x1) (add_SNo (minus_SNo x0) (minus_SNo x1))
Apply add_SNo_minus_SNo_rinv with add_SNo x0 x1, λ x2 x3 . x3 = add_SNo (add_SNo x0 x1) (add_SNo (minus_SNo x0) (minus_SNo x1)) leaving 2 subgoals.
The subproof is completed by applying L4.
Apply add_SNo_assoc with add_SNo x0 x1, minus_SNo x0, minus_SNo x1, λ x2 x3 . 0 = x3 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply add_SNo_com with x0, x1, λ x2 x3 . 0 = add_SNo (add_SNo x3 (minus_SNo x0)) (minus_SNo x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply add_SNo_assoc with x1, x0, minus_SNo x0, λ x2 x3 . 0 = add_SNo x2 (minus_SNo x1) leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying L2.
Apply add_SNo_minus_SNo_rinv with x0, λ x2 x3 . 0 = add_SNo (add_SNo x1 x3) (minus_SNo x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_SNo_0R with x1, λ x2 x3 . 0 = add_SNo x3 (minus_SNo x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply add_SNo_minus_SNo_rinv with x1, λ x2 x3 . 0 = x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ιιο be given.
Assume H5: x2 0 0.
The subproof is completed by applying H5.
Apply add_SNo_cancel_L with add_SNo x0 x1, minus_SNo (add_SNo x0 x1), add_SNo (minus_SNo x0) (minus_SNo x1) leaving 4 subgoals.
The subproof is completed by applying L4.
Apply SNo_minus_SNo with add_SNo x0 x1.
The subproof is completed by applying L4.
Apply SNo_add_SNo with minus_SNo x0, minus_SNo x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L5.