Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Claim L1: ...
...
Claim L2: ...
...
Claim L3: SNo x0
Apply ordinal_SNo with ....
...
Claim L4: ∀ x1 . nat_p x1 ⟶ mul_nat x0 x1 = mul_SNo x0 x1
Apply nat_ind with λ x1 . mul_nat x0 x1 = mul_SNo x0 x1 leaving 2 subgoals.
Apply mul_SNo_zeroR with x0, λ x1 x2 . mul_nat x0 0 = x2 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying mul_nat_0R with x0.
Let x1 of type ι be given.
Assume H4: nat_p x1.
Assume H5: mul_nat x0 x1 = mul_SNo x0 x1.
set y2 to be mul_nat x0 (ordsucc x1)
set y3 to be mul_SNo x1 (ordsucc y2)
Claim L6: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2
Let x4 of type ι → ο be given.
Assume H6: x4 (mul_SNo y2 (ordsucc y3)).
Apply mul_nat_SR with y2, y3, λ x5 . x4 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply add_nat_add_SNo with y2, mul_nat y2 y3, λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_p_omega with mul_nat y2 y3.
Apply mul_nat_p with y2, y3 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H4.
set y5 to be add_SNo y2 (mul_nat y2 y3)
set y6 to be add_SNo y3 (mul_SNo y3 x4)
Claim L7: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H7: x7 (add_SNo x4 (mul_SNo x4 y5)).
set y8 to be λ x8 . x7
Apply H5 with λ x9 x10 . y8 (add_SNo x4 x9) (add_SNo x4 x10).
The subproof is completed by applying H7.
set y7 to be λ x7 . y6
Apply L7 with λ x8 . y7 x8 y6 ⟶ y7 y6 x8 leaving 2 subgoals.
Assume H8: y7 y6 y6.
The subproof is completed by applying H8.
set y8 to be λ x8 . y7
Apply add_SNo_0L with y6, λ x9 x10 . mul_SNo y5 (ordsucc x9) = add_SNo y5 (mul_SNo y5 y6), λ x9 x10 . y8 x10 x9 leaving 3 subgoals.
Apply ordinal_SNo with y6.
Apply nat_p_ordinal with y6.
The subproof is completed by applying H5.
Apply add_SNo_ordinal_SL with 0, y6, λ x9 x10 . mul_SNo y5 x9 = add_SNo y5 (mul_SNo y5 y6) leaving 3 subgoals.
The subproof is completed by applying ordinal_Empty.
Apply nat_p_ordinal with y6.
The subproof is completed by applying H5.
Apply mul_SNo_distrL with y5, 1, y6, λ x9 x10 . x10 = add_SNo y5 (mul_SNo y5 y6) leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying SNo_1.
Apply ordinal_SNo with y6.
Apply nat_p_ordinal with y6.
The subproof is completed by applying H5.
set y9 to be add_SNo (mul_SNo y5 1) (mul_SNo y5 y6)
set y10 to be add_SNo y6 (mul_SNo y6 y7)
Claim L8: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
Assume H8: x11 (add_SNo y7 (mul_SNo y7 y8)).
set y12 to be λ x12 . x11
Apply mul_SNo_oneR with y7, λ x13 x14 . y12 (add_SNo x13 (mul_SNo y7 y8)) (add_SNo x14 (mul_SNo y7 y8)) leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Let x11 of type ι → ι → ο be given.
Apply L8 with λ x12 . x11 x12 y10 ⟶ x11 y10 x12.
Assume H9: x11 y10 y10.
The subproof is completed by applying H9.
The subproof is completed by applying L7.
Let x4 of type ι → ι → ο be given.
Apply L6 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H7: x4 y3 y3.
The subproof is completed by applying H7.
Let x1 of type ι be given.
Assume H5: x1 ∈ omega.
Apply L4 with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H5.
■