Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: c7ce4.. x0.
Claim L1: SNo (minus_SNo (28f8d.. x0))
Apply SNo_minus_SNo with 28f8d.. x0.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with x0.
The subproof is completed by applying H0.
Claim L2: SNo (minus_SNo (d634d.. x0))
Apply SNo_minus_SNo with d634d.. x0.
Apply unknownprop_f319423ed101339f42129d35c36f78ec84ab916352e52ec279686150bcbdfec5 with x0.
The subproof is completed by applying H0.
Apply unknownprop_be33d753151483c7bac1e70b0036b153d449838792ed17caa64a7328dfc698e0 with minus_SNo (28f8d.. x0), minus_SNo (d634d.. x0), λ x1 x2 . ad280.. (add_SNo (28f8d.. x0) x2) (add_SNo (d634d.. x0) (d634d.. (ad280.. (minus_SNo (28f8d.. x0)) (minus_SNo (d634d.. x0))))) = 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply unknownprop_a297e56f8bdca4759c242f4239a030f8b8676cee62a6758763e7f37b72905c22 with minus_SNo (28f8d.. x0), minus_SNo (d634d.. x0), λ x1 x2 . ad280.. (add_SNo (28f8d.. x0) (minus_SNo (28f8d.. x0))) (add_SNo (d634d.. x0) x2) = 0 leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply add_SNo_minus_SNo_rinv with 28f8d.. x0, λ x1 x2 . ad280.. x2 (add_SNo (d634d.. x0) (minus_SNo (d634d.. x0))) = 0 leaving 2 subgoals.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with x0.
The subproof is completed by applying H0.
Apply add_SNo_minus_SNo_rinv with d634d.. x0, λ x1 x2 . ad280.. 0 x2 = 0 leaving 2 subgoals.
Apply unknownprop_f319423ed101339f42129d35c36f78ec84ab916352e52ec279686150bcbdfec5 with x0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_872273e895264b163d3a3b042c5d1abf262e26919401a643ccce2dcdcb6a14ef with 0.
■