Search for blocks/addresses/...

Proofgold Proof

pf
Apply add_SNo_cancel_R with add_SNo u24 (minus_SNo u20), u20, u4 leaving 4 subgoals.
Apply SNo_add_SNo with u24, minus_SNo u20 leaving 2 subgoals.
Apply nat_p_SNo with u24.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
Apply SNo_minus_SNo with u20.
Apply nat_p_SNo with u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply nat_p_SNo with u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply nat_p_SNo with u4.
The subproof is completed by applying nat_4.
Apply add_SNo_minus_R2' with u24, u20, λ x0 x1 . x1 = add_SNo u4 u20 leaving 3 subgoals.
Apply nat_p_SNo with u24.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
Apply nat_p_SNo with u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Let x0 of type ιιο be given.
Apply add_SNo_com with u4, u20, λ x1 x2 . x2 = u24, λ x1 x2 . x0 x2 x1 leaving 3 subgoals.
Apply nat_p_SNo with u4.
The subproof is completed by applying nat_4.
Apply nat_p_SNo with u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply add_nat_add_SNo with u20, u4, λ x1 x2 . x1 = u24 leaving 3 subgoals.
Apply nat_p_omega with u20.
The subproof is completed by applying unknownprop_07ad204b3b4fc2b51cd8392b0e6a88916124d7f0f3dbf696bec5a683b0ea9dae.
Apply nat_p_omega with u4.
The subproof is completed by applying nat_4.
The subproof is completed by applying unknownprop_e7a22d56172b83cc5d886239f486a15dd72ae38e01e724bdd7d4045095e9b394.