[STATEMENT]
lemma exp_golomb_encoding: "is_encoding N\<^sub>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
have "is_encoding (\<lambda>n. N\<^sub>e n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
unfolding N\<^sub>e_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_encoding (\<lambda>n. Ng\<^sub>e (n + 1))
[PROOF STEP]
by (intro encoding_compose_2[where g="(\<lambda>n. n + 1)"] elias_gamma_encoding, auto)
[PROOF STATE]
proof (state)
this:
is_encoding N\<^sub>e

goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_encoding N\<^sub>e

goal (1 subgoal):
 1. is_encoding N\<^sub>e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_encoding N\<^sub>e

goal:
No subgoals!
[PROOF STEP]
qed