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_max_of (SNoL x0) x1.
Apply H1 with ∀ x2 . SNo x2SNoLt x0 x2SNoLt (add_SNo x1 x2) (add_SNo x0 x0)∃ x3 . and (x3SNoR x2) (add_SNo x1 x3 = add_SNo x0 x0).
Assume H2: and (x1SNoL x0) (SNo x1).
Apply H2 with (∀ x2 . x2SNoL x0SNo x2SNoLe x2 x1)∀ x2 . SNo x2SNoLt x0 x2SNoLt (add_SNo x1 x2) (add_SNo x0 x0)∃ x3 . and (x3SNoR x2) (add_SNo x1 x3 = add_SNo x0 x0).
Assume H3: x1SNoL x0.
Assume H4: SNo x1.
Assume H5: ∀ x2 . x2SNoL x0SNo x2SNoLe x2 x1.
Apply SNoL_E with x0, x1, ∀ x2 . SNo x2SNoLt x0 x2SNoLt (add_SNo x1 x2) (add_SNo x0 x0)∃ x3 . and (x3SNoR x2) (add_SNo x1 x3 = add_SNo x0 x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Assume H6: SNo x1.
Assume H7: SNoLev x1SNoLev x0.
Assume H8: SNoLt x1 x0.
Apply SNoLev_ind with λ x2 . SNoLt x0 x2SNoLt (add_SNo x1 x2) (add_SNo x0 x0)∃ x3 . and (x3SNoR x2) (add_SNo x1 x3 = add_SNo x0 x0).
Let x2 of type ι be given.
Assume H9: SNo x2.
Assume H10: ∀ x3 . x3SNoS_ (SNoLev x2)SNoLt x0 x3SNoLt (add_SNo x1 x3) (add_SNo x0 x0)∃ x4 . and (x4SNoR x3) (add_SNo x1 x4 = add_SNo x0 x0).
Assume H11: SNoLt x0 x2.
Assume H12: SNoLt (add_SNo x1 x2) (add_SNo x0 x0).
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Apply SNoLt_SNoL_or_SNoR_impred with add_SNo x1 x2, add_SNo x0 x0, ∃ x3 . and (x3SNoR x2) (add_SNo x1 x3 = add_SNo x0 x0) leaving 6 subgoals.
Apply SNo_add_SNo with x1, x2 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
The subproof is completed by applying L13.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Assume H17: x3SNoL (add_SNo x0 x0).
Assume H18: x3SNoR (add_SNo x1 x2).
Apply SNoL_E with add_SNo x0 x0, x3, ∃ x4 . and (x4SNoR x2) (add_SNo x1 x4 = add_SNo x0 x0) leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying H17.
Assume H19: SNo x3.
Assume H20: SNoLev x3SNoLev (add_SNo ... ...).
...
...
...