[STATEMENT]
lemma all_formulas_of_size: "F \<in> all_formulas_of_size K n \<longleftrightarrow> (size F \<le> Suc n \<and> atoms F \<subseteq> K)" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F \<in> all_formulas_of_size K n) = (size F \<le> Suc n \<and> atoms F \<subseteq> K)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (F \<in> all_formulas_of_size K n) = (size F \<le> Suc n \<and> atoms F \<subseteq> K)
[PROOF STEP]
have rl: "?r \<Longrightarrow> ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n
[PROOF STEP]
proof(induction F arbitrary: n)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x n. size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K \<Longrightarrow> Atom x \<in> all_formulas_of_size K n
 2. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 3. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 6. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (Atom x)
[PROOF STATE]
proof (state)
this:
size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K

goal (6 subgoals):
 1. \<And>x n. size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K \<Longrightarrow> Atom x \<in> all_formulas_of_size K n
 2. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 3. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 6. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have *: "Atom x \<in> all_formulas_of_size K 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Atom x \<in> all_formulas_of_size K 0
[PROOF STEP]
using Atom
[PROOF STATE]
proof (prove)
using this:
size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K

goal (1 subgoal):
 1. Atom x \<in> all_formulas_of_size K 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Atom x \<in> all_formulas_of_size K 0

goal (6 subgoals):
 1. \<And>x n. size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K \<Longrightarrow> Atom x \<in> all_formulas_of_size K n
 2. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 3. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 6. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
hence **: "Atom x \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc m])" for m
[PROOF STATE]
proof (prove)
using this:
Atom x \<in> all_formulas_of_size K 0

goal (1 subgoal):
 1. Atom x \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc m])
[PROOF STEP]
by (simp; metis atLeastLessThan_iff le_zero_eq not_le)
[PROOF STATE]
proof (state)
this:
Atom x \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])

goal (6 subgoals):
 1. \<And>x n. size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K \<Longrightarrow> Atom x \<in> all_formulas_of_size K n
 2. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 3. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 6. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Atom x \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])

goal (1 subgoal):
 1. Atom x \<in> all_formulas_of_size K n
[PROOF STEP]
using Atom
[PROOF STATE]
proof (prove)
using this:
Atom x \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])
size (Atom x) \<le> Suc n \<and> atoms (Atom x) \<subseteq> K

goal (1 subgoal):
 1. Atom x \<in> all_formulas_of_size K n
[PROOF STEP]
by(cases n; simp)
[PROOF STATE]
proof (state)
this:
Atom x \<in> all_formulas_of_size K n

goal (5 subgoals):
 1. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 2. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 2. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case Bot
[PROOF STATE]
proof (state)
this:
size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K

goal (5 subgoals):
 1. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 2. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have *: "Bot \<in> all_formulas_of_size K 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<in> all_formulas_of_size K 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bottom> \<in> all_formulas_of_size K 0

goal (5 subgoals):
 1. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 2. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
hence **: "Bot \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc m])" for m
[PROOF STATE]
proof (prove)
using this:
\<bottom> \<in> all_formulas_of_size K 0

goal (1 subgoal):
 1. \<bottom> \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc m])
[PROOF STEP]
by (simp; metis atLeastLessThan_iff le_zero_eq not_le)
[PROOF STATE]
proof (state)
this:
\<bottom> \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])

goal (5 subgoals):
 1. \<And>n. size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K \<Longrightarrow> \<bottom> \<in> all_formulas_of_size K n
 2. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 5. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bottom> \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<bottom> \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])

goal (1 subgoal):
 1. \<bottom> \<in> all_formulas_of_size K n
[PROOF STEP]
using Bot
[PROOF STATE]
proof (prove)
using this:
\<bottom> \<in> \<Union> (all_formulas_of_size K ` set [0..<Suc ?m])
size \<bottom> \<le> Suc n \<and> atoms \<bottom> \<subseteq> K

goal (1 subgoal):
 1. \<bottom> \<in> all_formulas_of_size K n
[PROOF STEP]
by(cases n; simp)
[PROOF STATE]
proof (state)
this:
\<bottom> \<in> all_formulas_of_size K n

goal (4 subgoals):
 1. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (Not F)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K

goal (4 subgoals):
 1. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have *: "size F \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size F \<le> n
[PROOF STEP]
using Not
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K

goal (1 subgoal):
 1. size F \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size F \<le> n

goal (4 subgoals):
 1. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F \<le> n
[PROOF STEP]
obtain m where n[simp]: "n = Suc m"
[PROOF STATE]
proof (prove)
using this:
size F \<le> n

goal (1 subgoal):
 1. (\<And>m. n = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (4 subgoals):
 1. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with Not
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K
n = Suc m
[PROOF STEP]
have IH: "F \<in> all_formulas_of_size K m"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K
n = Suc m

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<in> all_formulas_of_size K m

goal (4 subgoals):
 1. \<And>F n. \<lbrakk>\<And>n. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n; size (\<^bold>\<not> F) \<le> Suc n \<and> atoms (\<^bold>\<not> F) \<subseteq> K\<rbrakk> \<Longrightarrow> \<^bold>\<not> F \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 4. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F \<in> all_formulas_of_size K m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K m

goal (1 subgoal):
 1. \<^bold>\<not> F \<in> all_formulas_of_size K n
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K m
size F \<le> n

goal (1 subgoal):
 1. \<^bold>\<not> F \<in> all_formulas_of_size K n
[PROOF STEP]
by(simp add: bexI[where x=F])
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> F \<in> all_formulas_of_size K n

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (And F G)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with And
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K
[PROOF STEP]
have *: "size F + size G \<le> n"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K

goal (1 subgoal):
 1. size F + size G \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size F + size G \<le> n

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F + size G \<le> n
[PROOF STEP]
obtain m where n[simp]: "n = Suc m"
[PROOF STATE]
proof (prove)
using this:
size F + size G \<le> n

goal (1 subgoal):
 1. (\<And>m. n = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc m
[PROOF STEP]
obtain nF nG where nFG[simp]: "size F \<le> nF" "size G \<le> nG" "n = nF + nG"
[PROOF STATE]
proof (prove)
using this:
n = Suc m

goal (1 subgoal):
 1. (\<And>nF nG. \<lbrakk>size F \<le> nF; size G \<le> nG; n = nF + nG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis * add.assoc nat_le_iff_add order_refl)
[PROOF STATE]
proof (state)
this:
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F \<le> nF
size G \<le> nG
n = nF + nG
[PROOF STEP]
obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
[PROOF STATE]
proof (prove)
using this:
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. (\<And>mF mG. \<lbrakk>nF = Suc mF; nG = Suc mG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
[PROOF STATE]
proof (state)
this:
nF = Suc mF
nG = Suc mG

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with And
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K
nF = Suc mF
nG = Suc mG
[PROOF STEP]
have IH: "F \<in> all_formulas_of_size K mF" "G \<in> all_formulas_of_size K mG"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K
nF = Suc mF
nG = Suc mG

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K mF &&& G \<in> all_formulas_of_size K mG
[PROOF STEP]
using nFG
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<and> G) \<le> Suc n \<and> atoms (F \<^bold>\<and> G) \<subseteq> K
nF = Suc mF
nG = Suc mG
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K mF &&& G \<in> all_formulas_of_size K mG
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
let ?af = "\<Union>(set [all_formulas_of_size K m. m \<leftarrow> [0..<Suc m]])"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have r: "F \<in> all_formulas_of_size K mF \<Longrightarrow> mF \<le> n \<Longrightarrow> F \<in> \<Union>(set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<in> all_formulas_of_size K mF; mF \<le> n\<rbrakk> \<Longrightarrow> F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc n]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?F \<in> all_formulas_of_size K ?mF; ?mF \<le> ?n\<rbrakk> \<Longrightarrow> ?F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc ?n]))

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have af: "F \<in> ?af" "G \<in> ?af"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m])) &&& G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
[PROOF STEP]
using nFG(3)
[PROOF STATE]
proof (prove)
using this:
n = nF + nG

goal (1 subgoal):
 1. F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m])) &&& G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
[PROOF STEP]
by(intro IH[THEN r]; simp)+
[PROOF STATE]
proof (state)
this:
F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have m: "F \<^bold>\<and> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<^bold>\<and> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
size F + size G \<le> n

goal (1 subgoal):
 1. F \<^bold>\<and> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<^bold>\<and> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})

goal (3 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<and> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<and> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<and> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 3. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
from IH *
[PROOF STATE]
proof (chain)
picking this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n

goal (1 subgoal):
 1. F \<^bold>\<and> G \<in> all_formulas_of_size K n
[PROOF STEP]
using af
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n
F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))

goal (1 subgoal):
 1. F \<^bold>\<and> G \<in> all_formulas_of_size K n
[PROOF STEP]
by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
[PROOF STATE]
proof (state)
this:
F \<^bold>\<and> G \<in> all_formulas_of_size K n

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (Or F G)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (Imp F G) \<comment> \<open>analogous\<close>
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (Or F G)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with Or
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K
[PROOF STEP]
have *: "size F + size G \<le> n"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K

goal (1 subgoal):
 1. size F + size G \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size F + size G \<le> n

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F + size G \<le> n
[PROOF STEP]
obtain m where n[simp]: "n = Suc m"
[PROOF STATE]
proof (prove)
using this:
size F + size G \<le> n

goal (1 subgoal):
 1. (\<And>m. n = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc m
[PROOF STEP]
obtain nF nG where nFG[simp]: "size F \<le> nF" "size G \<le> nG" "n = nF + nG"
[PROOF STATE]
proof (prove)
using this:
n = Suc m

goal (1 subgoal):
 1. (\<And>nF nG. \<lbrakk>size F \<le> nF; size G \<le> nG; n = nF + nG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis * add.assoc nat_le_iff_add order_refl)
[PROOF STATE]
proof (state)
this:
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F \<le> nF
size G \<le> nG
n = nF + nG
[PROOF STEP]
obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
[PROOF STATE]
proof (prove)
using this:
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. (\<And>mF mG. \<lbrakk>nF = Suc mF; nG = Suc mG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
[PROOF STATE]
proof (state)
this:
nF = Suc mF
nG = Suc mG

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with Or
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K
nF = Suc mF
nG = Suc mG
[PROOF STEP]
have IH: "F \<in> all_formulas_of_size K mF" "G \<in> all_formulas_of_size K mG"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K
nF = Suc mF
nG = Suc mG

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K mF &&& G \<in> all_formulas_of_size K mG
[PROOF STEP]
using nFG
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<or> G) \<le> Suc n \<and> atoms (F \<^bold>\<or> G) \<subseteq> K
nF = Suc mF
nG = Suc mG
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K mF &&& G \<in> all_formulas_of_size K mG
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
let ?af = "\<Union>(set [all_formulas_of_size K m. m \<leftarrow> [0..<Suc m]])"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have r: "F \<in> all_formulas_of_size K mF \<Longrightarrow> mF \<le> n \<Longrightarrow> F \<in> \<Union>(set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<in> all_formulas_of_size K mF; mF \<le> n\<rbrakk> \<Longrightarrow> F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc n]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?F \<in> all_formulas_of_size K ?mF; ?mF \<le> ?n\<rbrakk> \<Longrightarrow> ?F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc ?n]))

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have af: "F \<in> ?af" "G \<in> ?af"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m])) &&& G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
[PROOF STEP]
using nFG(3)
[PROOF STATE]
proof (prove)
using this:
n = nF + nG

goal (1 subgoal):
 1. F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m])) &&& G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
[PROOF STEP]
by(intro IH[THEN r]; simp)+
[PROOF STATE]
proof (state)
this:
F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have m: "Or F G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<^bold>\<or> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
size F + size G \<le> n

goal (1 subgoal):
 1. F \<^bold>\<or> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<^bold>\<or> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})

goal (2 subgoals):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<or> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<or> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<or> F2 \<in> all_formulas_of_size K n
 2. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
from IH *
[PROOF STATE]
proof (chain)
picking this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n

goal (1 subgoal):
 1. F \<^bold>\<or> G \<in> all_formulas_of_size K n
[PROOF STEP]
using af
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n
F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))

goal (1 subgoal):
 1. F \<^bold>\<or> G \<in> all_formulas_of_size K n
[PROOF STEP]
by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
[PROOF STATE]
proof (state)
this:
F \<^bold>\<or> G \<in> all_formulas_of_size K n

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
case (Imp F G)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with Imp
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K
[PROOF STEP]
have *: "size F + size G \<le> n"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K

goal (1 subgoal):
 1. size F + size G \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
size F + size G \<le> n

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F + size G \<le> n
[PROOF STEP]
obtain m where n[simp]: "n = Suc m"
[PROOF STATE]
proof (prove)
using this:
size F + size G \<le> n

goal (1 subgoal):
 1. (\<And>m. n = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 add_is_0 formula.size_neq le_zero_eq neq0_conv)
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc m
[PROOF STEP]
obtain nF nG where nFG[simp]: "size F \<le> nF" "size G \<le> nG" "n = nF + nG"
[PROOF STATE]
proof (prove)
using this:
n = Suc m

goal (1 subgoal):
 1. (\<And>nF nG. \<lbrakk>size F \<le> nF; size G \<le> nG; n = nF + nG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis * add.assoc nat_le_iff_add order_refl)
[PROOF STATE]
proof (state)
this:
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
size F \<le> nF
size G \<le> nG
n = nF + nG
[PROOF STEP]
obtain mF mG where mFG[simp]: "nF = Suc mF" "nG = Suc mG"
[PROOF STATE]
proof (prove)
using this:
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. (\<And>mF mG. \<lbrakk>nF = Suc mF; nG = Suc mG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_diff_1 formula.size_neq leD neq0_conv)
[PROOF STATE]
proof (state)
this:
nF = Suc mF
nG = Suc mG

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
with Imp
[PROOF STATE]
proof (chain)
picking this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K
nF = Suc mF
nG = Suc mG
[PROOF STEP]
have IH: "F \<in> all_formulas_of_size K mF" "G \<in> all_formulas_of_size K mG"
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K
nF = Suc mF
nG = Suc mG

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K mF &&& G \<in> all_formulas_of_size K mG
[PROOF STEP]
using nFG
[PROOF STATE]
proof (prove)
using this:
size F \<le> Suc ?n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K ?n
size G \<le> Suc ?n \<and> atoms G \<subseteq> K \<Longrightarrow> G \<in> all_formulas_of_size K ?n
size (F \<^bold>\<rightarrow> G) \<le> Suc n \<and> atoms (F \<^bold>\<rightarrow> G) \<subseteq> K
nF = Suc mF
nG = Suc mG
size F \<le> nF
size G \<le> nG
n = nF + nG

goal (1 subgoal):
 1. F \<in> all_formulas_of_size K mF &&& G \<in> all_formulas_of_size K mG
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
let ?af = "\<Union>(set [all_formulas_of_size K m. m \<leftarrow> [0..<Suc m]])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have r: "F \<in> all_formulas_of_size K mF \<Longrightarrow> mF \<le> n \<Longrightarrow> F \<in> \<Union>(set (map (all_formulas_of_size K) [0..<Suc n]))"
      for F mF n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<in> all_formulas_of_size K mF; mF \<le> n\<rbrakk> \<Longrightarrow> F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc n]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?F \<in> all_formulas_of_size K ?mF; ?mF \<le> ?n\<rbrakk> \<Longrightarrow> ?F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc ?n]))

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have af: "F \<in> ?af" "G \<in> ?af"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m])) &&& G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
[PROOF STEP]
using nFG(3)
[PROOF STATE]
proof (prove)
using this:
n = nF + nG

goal (1 subgoal):
 1. F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m])) &&& G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
[PROOF STEP]
by(intro IH[THEN r]; simp)+
[PROOF STATE]
proof (state)
this:
F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
have m: "Imp F G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
size F + size G \<le> n

goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F \<^bold>\<rightarrow> G \<in> (if size F + size G \<le> Suc m then {F \<^bold>\<and> G, F \<^bold>\<or> G, F \<^bold>\<rightarrow> G} else {})

goal (1 subgoal):
 1. \<And>F1 F2 n. \<lbrakk>\<And>n. size F1 \<le> Suc n \<and> atoms F1 \<subseteq> K \<Longrightarrow> F1 \<in> all_formulas_of_size K n; \<And>n. size F2 \<le> Suc n \<and> atoms F2 \<subseteq> K \<Longrightarrow> F2 \<in> all_formulas_of_size K n; size (F1 \<^bold>\<rightarrow> F2) \<le> Suc n \<and> atoms (F1 \<^bold>\<rightarrow> F2) \<subseteq> K\<rbrakk> \<Longrightarrow> F1 \<^bold>\<rightarrow> F2 \<in> all_formulas_of_size K n
[PROOF STEP]
from IH *
[PROOF STATE]
proof (chain)
picking this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n

goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<in> all_formulas_of_size K n
[PROOF STEP]
using af
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K mF
G \<in> all_formulas_of_size K mG
size F + size G \<le> n
F \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))
G \<in> \<Union> (set (map (all_formulas_of_size K) [0..<Suc m]))

goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<in> all_formulas_of_size K n
[PROOF STEP]
by(simp only: n all_formulas_of_size.simps Let_def, insert m) fast
[PROOF STATE]
proof (state)
this:
F \<^bold>\<rightarrow> G \<in> all_formulas_of_size K n

goal:
No subgoals!
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (state)
this:
F \<^bold>\<rightarrow> G \<in> all_formulas_of_size K n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n

goal (1 subgoal):
 1. (F \<in> all_formulas_of_size K n) = (size F \<le> Suc n \<and> atoms F \<subseteq> K)
[PROOF STEP]
have lr: ?r if l: ?l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size F \<le> Suc n \<and> atoms F \<subseteq> K
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. size F \<le> Suc n
 2. atoms F \<subseteq> K
[PROOF STEP]
have *: "F \<in> all_formulas_of_size K x \<Longrightarrow> F \<in> all_formulas_of_size K (x + n)" for x n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> all_formulas_of_size K x \<Longrightarrow> F \<in> all_formulas_of_size K (x + n)
[PROOF STEP]
by(induction n; simp)
[PROOF STATE]
proof (state)
this:
F \<in> all_formulas_of_size K ?x \<Longrightarrow> F \<in> all_formulas_of_size K (?x + ?n)

goal (2 subgoals):
 1. size F \<le> Suc n
 2. atoms F \<subseteq> K
[PROOF STEP]
show "size F \<le> Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size F \<le> Suc n
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K n

goal (1 subgoal):
 1. size F \<le> Suc n
[PROOF STEP]
by(induction n; auto split: if_splits) (metis "*" le_SucI le_eq_less_or_eq le_iff_add)
[PROOF STATE]
proof (state)
this:
size F \<le> Suc n

goal (1 subgoal):
 1. atoms F \<subseteq> K
[PROOF STEP]
show "atoms F \<subseteq> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms F \<subseteq> K
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K n

goal (1 subgoal):
 1. atoms F \<subseteq> K
[PROOF STEP]
proof(induction n arbitrary: F rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
case (less x)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x

goal (1 subgoal):
 1. atoms F \<subseteq> K
[PROOF STEP]
proof(cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = 0\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
 2. \<And>nat. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = Suc nat\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = 0\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
 2. \<And>nat. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = Suc nat\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x
x = 0

goal (1 subgoal):
 1. atoms F \<subseteq> K
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
atoms F \<subseteq> K

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = Suc nat\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = Suc nat\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
case (Suc y)
[PROOF STATE]
proof (state)
this:
x = Suc y

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<And>y F. \<lbrakk>y < x; F \<in> all_formulas_of_size K y\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K; F \<in> all_formulas_of_size K x; x = Suc nat\<rbrakk> \<Longrightarrow> atoms F \<subseteq> K
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x
x = Suc y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y < x; ?F \<in> all_formulas_of_size K ?y\<rbrakk> \<Longrightarrow> atoms ?F \<subseteq> K
F \<in> all_formulas_of_size K x
x = Suc y

goal (1 subgoal):
 1. atoms F \<subseteq> K
[PROOF STEP]
by(simp only: all_formulas_of_size.simps Let_def) (fastforce simp add: less_Suc_eq split: if_splits)
[PROOF STATE]
proof (state)
this:
atoms F \<subseteq> K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atoms F \<subseteq> K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atoms F \<subseteq> K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
F \<in> all_formulas_of_size K n \<Longrightarrow> size F \<le> Suc n \<and> atoms F \<subseteq> K

goal (1 subgoal):
 1. (F \<in> all_formulas_of_size K n) = (size F \<le> Suc n \<and> atoms F \<subseteq> K)
[PROOF STEP]
from lr rl
[PROOF STATE]
proof (chain)
picking this:
F \<in> all_formulas_of_size K n \<Longrightarrow> size F \<le> Suc n \<and> atoms F \<subseteq> K
size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F \<in> all_formulas_of_size K n \<Longrightarrow> size F \<le> Suc n \<and> atoms F \<subseteq> K
size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> F \<in> all_formulas_of_size K n

goal (1 subgoal):
 1. (F \<in> all_formulas_of_size K n) = (size F \<le> Suc n \<and> atoms F \<subseteq> K)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F \<in> all_formulas_of_size K n \<Longrightarrow> F \<in> all_formulas_of_size K n
 2. size F \<le> Suc n \<and> atoms F \<subseteq> K \<Longrightarrow> size F \<le> Suc n \<and> atoms F \<subseteq> K
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(F \<in> all_formulas_of_size K n) = (size F \<le> Suc n \<and> atoms F \<subseteq> K)

goal:
No subgoals!
[PROOF STEP]
qed