Let x0 of type ι be given.

Assume H0: CRing_with_id x0.

Claim L1: ∀ x1 . nat_p x1 ⟶ ∀ x2 . (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ field0 x0) ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ CRing_with_id_eval_poly x0 x1 x2 x3 ∈ field0 x0

Apply nat_ind with λ x1 . ∀ x2 . (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ field0 x0) ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ CRing_with_id_eval_poly x0 x1 x2 x3 ∈ field0 x0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H1: ∀ x2 . x2 ∈ 0 ⟶ ap x1 x2 ∈ field0 x0.

Let x2 of type ι be given.

Assume H2: x2 ∈ field0 x0.

Apply nat_primrec_0 with field3 x0, λ x3 x4 . field1b x0 (field2b x0 (ap x1 x3) (CRing_with_id_omega_exp x0 x2 x3)) x4, λ x3 x4 . x4 ∈ field0 x0.

Apply CRing_with_id_zero_In with x0.

The subproof is completed by applying H0.

Let x1 of type ι be given.

Assume H1: nat_p x1.

Assume H2: ∀ x2 . (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 ∈ field0 x0) ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ CRing_with_id_eval_poly x0 x1 x2 x3 ∈ field0 x0.

Let x2 of type ι be given.

Assume H3: ∀ x3 . x3 ∈ ordsucc x1 ⟶ ap x2 x3 ∈ field0 x0.

Let x3 of type ι be given.

Assume H4: x3 ∈ field0 x0.

Apply nat_primrec_S with field3 x0, λ x4 x5 . field1b x0 (field2b x0 (ap x2 x4) (CRing_with_id_omega_exp x0 x3 x4)) x5, x1, λ x4 x5 . x5 ∈ field0 x0 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply CRing_with_id_plus_clos with x0, field2b x0 (ap x2 x1) (CRing_with_id_omega_exp x0 x3 x1), nat_primrec (field3 x0) (λ x4 x5 . field1b x0 (field2b x0 (ap x2 x4) (CRing_with_id_omega_exp x0 x3 x4)) x5) x1 leaving 3 subgoals.

The subproof is completed by applying H0.

Apply CRing_with_id_mult_clos with x0, ap x2 x1, CRing_with_id_omega_exp x0 x3 x1 leaving 3 subgoals.

The subproof is completed by applying H0.

Apply H3 with x1.

The subproof is completed by applying ordsuccI2 with x1.

Apply CRing_with_id_omega_exp_clos with x0, x3, x1 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H4.

Apply nat_p_omega with x1.

The subproof is completed by applying H1.

Claim L5: ∀ x4 . x4 ∈ x1 ⟶ ap x2 x4 ∈ field0 x0

Let x4 of type ι be given.

Assume H5: x4 ∈ x1.

Apply H3 with x4.

Apply ordsuccI1 with x1, x4.

The subproof is completed by applying H5.

Apply H2 with x2, x3 leaving 2 subgoals.

The subproof is completed by applying L5.

The subproof is completed by applying H4.

Let x1 of type ι be given.

Assume H2: x1 ∈ omega.

Let x2 of type ι be given.

Assume H3: x2 ∈ setexp (field0 x0) x1.

Apply L1 with x1, x2 leaving 2 subgoals.

Apply omega_nat_p with x1.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Assume H4: x3 ∈ x1.

Apply ap_Pi with x1, λ x4 . field0 x0, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

■

Proofgold Proof