Apply nat_ind with λ x0 . ordsucc (exp_nat 2 (ordsucc x0)) ∈ exp_nat 2 (ordsucc (ordsucc x0)) leaving 2 subgoals.

Apply unknownprop_5858d8b36c7cdaccd2f26eae0cf9cb2cc1dc7fc685e15eee42b07d14732d6e73 with 2, λ x0 x1 . ordsucc x1 ∈ exp_nat 2 2.

Apply unknownprop_c2aa62c368a47ae018ac0952ff3137b0b6dc17b9b871ce9eb89fc53a8a9f308f with λ x0 x1 . 3 ∈ x1.

The subproof is completed by applying In_3_4.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ordsucc (exp_nat 2 (ordsucc x0)) ∈ exp_nat 2 (ordsucc (ordsucc x0)).

Apply nat_primrec_S with 1, λ x1 x2 . mul_nat 2 x2, ordsucc x0, λ x1 x2 . ordsucc x2 ∈ exp_nat 2 (ordsucc (ordsucc (ordsucc x0))) leaving 2 subgoals.

Apply nat_ordsucc with x0.

The subproof is completed by applying H0.

Apply nat_primrec_S with 1, λ x1 x2 . mul_nat 2 x2, ordsucc (ordsucc x0), λ x1 x2 . ordsucc (mul_nat 2 (exp_nat 2 (ordsucc x0))) ∈ x2 leaving 2 subgoals.

Apply nat_ordsucc with ordsucc x0.

Apply nat_ordsucc with x0.

The subproof is completed by applying H0.

Claim L2: nat_p (exp_nat 2 (ordsucc (ordsucc x0)))

Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with 2, ordsucc (ordsucc x0) leaving 2 subgoals.

The subproof is completed by applying nat_2.

Apply nat_ordsucc with ordsucc x0.

Apply nat_ordsucc with x0.

The subproof is completed by applying H0.

Apply unknownprop_98467c341abf2d4df00f25d8d19317397055bbc0ea96a9fffe28da9dc82a28f5 with exp_nat 2 (ordsucc (ordsucc x0)), exp_nat 2 (ordsucc x0) leaving 2 subgoals.

The subproof is completed by applying L2.

Apply nat_trans with exp_nat 2 (ordsucc (ordsucc x0)), ordsucc (exp_nat 2 (ordsucc x0)), exp_nat 2 (ordsucc x0) leaving 3 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying H1.

The subproof is completed by applying ordsuccI2 with exp_nat 2 (ordsucc x0).

■

Proofgold Proof