Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Apply nat_ind with λ x1 . ∀ x2 x3 . atleastp (add_nat x0 x1) (binunion x2 x3)or (atleastp x0 x2) (atleastp x1 x3) leaving 2 subgoals.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply add_nat_0R with x0, λ x3 x4 . atleastp x4 (binunion x1 x2)or (atleastp x0 x1) (atleastp 0 x2).
Assume H1: atleastp x0 (binunion x1 x2).
Apply orIR with atleastp x0 x1, atleastp 0 x2.
The subproof is completed by applying unknownprop_b7030c4d179dca75b1c0a5a2dab6748493aebd2d7f37d4cf7a0d3bf2081224c9 with x2.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: ∀ x2 x3 . atleastp (add_nat x0 x1) (binunion x2 x3)or (atleastp x0 x2) (atleastp x1 x3).
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply add_nat_SR with x0, x1, λ x4 x5 . atleastp x5 (binunion x2 x3)or (atleastp x0 x2) (atleastp (ordsucc x1) x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: atleastp (ordsucc (add_nat x0 x1)) (binunion x2 x3).
Apply H3 with or (atleastp x0 x2) (atleastp (ordsucc x1) x3).
Let x4 of type ιι be given.
Assume H4: inj (ordsucc (add_nat x0 x1)) (binunion x2 x3) x4.
Apply H4 with or (atleastp x0 x2) (atleastp (ordsucc x1) x3).
Assume H5: ∀ x5 . x5ordsucc (add_nat x0 x1)x4 x5binunion x2 x3.
Assume H6: ∀ x5 . x5ordsucc (add_nat x0 x1)∀ x6 . x6ordsucc (add_nat x0 x1)x4 x5 = x4 x6x5 = x6.
Apply xm with ∀ x5 . x5x0x4 x5x2, or (atleastp x0 x2) (atleastp (ordsucc x1) x3) leaving 2 subgoals.
Assume H7: ∀ x5 . x5x0x4 x5x2.
Apply orIL with atleastp x0 x2, atleastp (ordsucc x1) x3.
Let x5 of type ο be given.
Assume H8: ∀ x6 : ι → ι . inj x0 x2 x6x5.
Apply H8 with x4.
Apply andI with ∀ x6 . x6x0x4 x6x2, ∀ x6 . x6x0∀ x7 . x7x0x4 x6 = x4 x7x6 = x7 leaving 2 subgoals.
The subproof is completed by applying H7.
Let x6 of type ι be given.
Assume H9: x6x0.
Let x7 of type ι be given.
Assume H10: x7x0.
Apply H6 with x6, x7 leaving 2 subgoals.
Apply ordsuccI1 with add_nat x0 x1, x6.
Apply unknownprop_2dcf4dd8557a0ffd2a187961d1bc330ef1aae42c546555814bac26eb5e3c6d68 with x0, x1, x6 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
Apply ordsuccI1 with add_nat x0 x1, x7.
Apply unknownprop_2dcf4dd8557a0ffd2a187961d1bc330ef1aae42c546555814bac26eb5e3c6d68 with x0, x1, x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H10.
Assume H7: not (∀ x5 . x5x0x4 x5x2).
Apply dneg with or (atleastp x0 x2) (atleastp (ordsucc x1) x3).
Assume H8: not ....
...