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.
Let x3 of type ι be given.
Assume H0: CSNo x0.
Assume H1: CSNo x1.
Assume H2: CSNo x2.
Assume H3: CSNo x3.
Apply unknownprop_cb3c73e6397c4921a333f973bae46a7e59f433123dea81f3a2d0adee769cf93f with x2, λ x4 x5 . add_CSNo (add_CSNo x0 (add_CSNo x1 (minus_CSNo x2))) (add_CSNo x4 x3) = add_CSNo x0 (add_CSNo x1 x3) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_25736a7f92c31e8fd99a310f6c7a28172c5f7a5b698118098169e99d8456d9ea with x0, x1, minus_CSNo x2, x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply CSNo_minus_CSNo with x2.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
■