Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0omega.
Apply nat_ind with λ x1 . add_SNo (minus_SNo x0) x1int leaving 2 subgoals.
Apply add_SNo_0R with minus_SNo x0, λ x1 x2 . x2int leaving 2 subgoals.
Apply SNo_minus_SNo with x0.
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply int_minus_SNo_omega with x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: add_SNo (minus_SNo x0) x1int.
Apply ordinal_ordsucc_SNo_eq with x1, λ x2 x3 . add_SNo (minus_SNo x0) x3int leaving 2 subgoals.
Apply nat_p_ordinal with x1.
The subproof is completed by applying H1.
Apply add_SNo_com_3_0_1 with minus_SNo x0, 1, x1, λ x2 x3 . x3int leaving 4 subgoals.
Apply SNo_minus_SNo with x0.
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_1.
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
The subproof is completed by applying H1.
Apply int_SNo_cases with λ x2 . add_SNo (minus_SNo x0) x1 = x2add_SNo 1 (add_SNo (minus_SNo x0) x1)int, add_SNo (minus_SNo x0) x1 leaving 4 subgoals.
Let x2 of type ι be given.
Assume H3: x2omega.
Assume H4: add_SNo (minus_SNo x0) x1 = x2.
Apply H4 with λ x3 x4 . add_SNo 1 x4int.
Apply ordinal_ordsucc_SNo_eq with x2, λ x3 x4 . x3int leaving 2 subgoals.
Apply nat_p_ordinal with x2.
Apply omega_nat_p with x2.
The subproof is completed by applying H3.
Apply Subq_omega_int with ordsucc x2.
Apply omega_ordsucc with x2.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H3: x2omega.
Assume H4: add_SNo (minus_SNo x0) x1 = minus_SNo x2.
Apply H4 with λ x3 x4 . add_SNo 1 x4int.
Apply nat_inv with x2, add_SNo 1 (minus_SNo x2)int leaving 3 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H3.
Assume H5: x2 = 0.
Apply H5 with λ x3 x4 . add_SNo 1 (minus_SNo x4)int.
Apply minus_SNo_0 with λ x3 x4 . add_SNo 1 x4int.
Apply add_SNo_0R with 1, λ x3 x4 . x4int leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply Subq_omega_int with 1.
Apply nat_p_omega with 1.
The subproof is completed by applying nat_1.
Assume H5: ∃ x3 . and (nat_p x3) (x2 = ordsucc x3).
Apply H5 with add_SNo 1 (minus_SNo x2)int.
Let x3 of type ι be given.
Assume H6: (λ x4 . and (nat_p x4) (x2 = ordsucc x4)) x3.
Apply H6 with add_SNo 1 (minus_SNo x2)int.
Assume H7: nat_p x3.
Assume H8: x2 = ordsucc x3.
Apply H8 with λ x4 x5 . add_SNo 1 (minus_SNo x5)int.
Apply ordinal_ordsucc_SNo_eq with x3, λ x4 x5 . add_SNo 1 (minus_SNo x5)int leaving 2 subgoals.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H7.
Apply minus_add_SNo_distr with 1, x3, λ x4 x5 . add_SNo 1 x5int leaving 3 subgoals.
The subproof is completed by applying SNo_1.
Apply ordinal_SNo with x3.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H7.
Apply add_SNo_minus_SNo_prop2 with 1, minus_SNo x3, λ x4 x5 . x5int leaving 3 subgoals.
The subproof is completed by applying SNo_1.
Apply SNo_minus_SNo with x3.
Apply ordinal_SNo with x3.
Apply nat_p_ordinal with x3.
The subproof is completed by applying H7.
Apply int_minus_SNo_omega with x3.
Apply nat_p_omega with x3.
The subproof is completed by applying H7.
The subproof is completed by applying H2.
set y2 to be add_SNo (minus_SNo x0) x1
Let x3 of type ιιο be given.
Assume H3: x3 y2 y2.
The subproof is completed by applying H3.