| pf |
|---|
Apply int_SNo_cases with λ x0 . ∀ x1 . x1 ∈ int ⟶ SNoLt x0 x1 ⟶ SNoLe (add_SNo x0 1) x1 leaving 2 subgoals.
Let x0 of type ι be given.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply nat_p_SNo with x0.
The subproof is completed by applying L1.
Apply int_SNo_cases with λ x1 . SNoLt x0 x1 ⟶ SNoLe (add_SNo x0 1) x1 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_1e19ea400270e16dd9b4d959fcd683273342d2b8620f41b2a847b00512981e9c with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply omega_nat_p with x1.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Apply omega_nat_p with x1.
The subproof is completed by applying H3.
Apply nat_p_SNo with x1.
The subproof is completed by applying L4.
Apply FalseE with SNoLe (add_SNo x0 1) (minus_SNo x1).
Apply SNoLt_irref with 0.
Apply SNoLeLt_tra with 0, x0, 0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with x0.
The subproof is completed by applying L1.
Apply SNoLtLe_tra with x0, minus_SNo x1, 0 leaving 5 subgoals.
The subproof is completed by applying L2.
Apply SNo_minus_SNo with x1.
The subproof is completed by applying L5.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H6.
Apply minus_SNo_0 with λ x2 x3 . SNoLe (minus_SNo x1) x2.
Apply minus_SNo_Le_contra with 0, x1 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying L5.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with x1.
The subproof is completed by applying L4.
Let x0 of type ι be given.
Apply int_SNo_cases with λ x1 . SNoLt (minus_SNo x0) x1 ⟶ SNoLe (add_SNo (minus_SNo x0) 1) x1 leaving 2 subgoals.
Let x1 of type ι be given.
Apply SNoLtLe_or with x1, add_SNo (minus_SNo x0) 1, SNoLe (add_SNo (minus_SNo x0) 1) x1 leaving 4 subgoals.
The subproof is completed by applying L6.
Apply SNo_add_SNo with minus_SNo x0, 1 leaving 2 subgoals.
Apply SNo_minus_SNo with x0.
The subproof is completed by applying L3.
The subproof is completed by applying SNo_1.
Claim L10: x1 = 0
Apply nat_inv_impred with λ x2 . x1 = x2 ⟶ x2 = 0, x1 leaving 4 subgoals.
Assume H10: x1 = 0.
Let x2 of type ι → ι → ο be given.
Assume H11: x2 0 0.
The subproof is completed by applying H11.
Let x2 of type ι be given.
Assume H10: ....
Apply L10 with λ x2 x3 . SNoLe (add_SNo (minus_SNo x0) 1) x3.
Apply nat_inv_impred with λ x2 . SNoLt (minus_SNo x2) 0 ⟶ SNoLe (add_SNo (minus_SNo x2) 1) 0, x0 leaving 4 subgoals.
Apply FalseE with SNoLe (add_SNo (minus_SNo 0) 1) 0.
Apply SNoLt_irref with 0.
Apply minus_SNo_0 with λ x2 x3 . SNoLt x2 0.
The subproof is completed by applying H11.
Let x2 of type ι be given.
Apply ordinal_ordsucc_SNo_eq with x2, λ x3 x4 . SNoLe (add_SNo (minus_SNo x4) 1) 0 leaving 2 subgoals.
Apply nat_p_ordinal with x2.
The subproof is completed by applying H11.
Apply add_SNo_com with 1, x2, λ x3 x4 . SNoLe (add_SNo (minus_SNo x4) 1) 0 leaving 3 subgoals.
The subproof is completed by applying SNo_1.
Apply nat_p_SNo with x2.
The subproof is completed by applying H11.
Apply minus_add_SNo_distr with x2, 1, λ x3 x4 . SNoLe (add_SNo x4 1) 0 leaving 3 subgoals.
Apply nat_p_SNo with x2.
The subproof is completed by applying H11.
The subproof is completed by applying SNo_1.
Apply add_SNo_minus_R2' with minus_SNo x2, 1, λ x3 x4 . SNoLe x4 0 leaving 3 subgoals.
Apply SNo_minus_SNo with x2.
Apply nat_p_SNo with x2.
The subproof is completed by applying H11.
The subproof is completed by applying SNo_1.
Apply minus_SNo_0 with λ x3 x4 . SNoLe (minus_SNo x2) x3.
Apply minus_SNo_Le_contra with 0, x2 leaving 3 subgoals.
The subproof is completed by applying SNo_0.
Apply nat_p_SNo with x2.
The subproof is completed by applying H11.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with x2.
The subproof is completed by applying H11.
The subproof is completed by applying L1.
Apply L10 with λ x2 x3 . SNoLt (minus_SNo x0) x2.
The subproof is completed by applying H7.
■ |
|