insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
have "\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth x\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth x\<^sub>1)
[PROOF STEP]
using F4
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<^sub>1. analz x\<^sub>1 \<subseteq> analz (synth x\<^sub>1)

goal (1 subgoal):
 1. \<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth x\<^sub>1)
[PROOF STEP]
by (metis analz_subset_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth x\<^sub>1)

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth (analz x\<^sub>1))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth x\<^sub>1)

goal (1 subgoal):
 1. \<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth (analz x\<^sub>1))
[PROOF STEP]
by (metis analz_subset_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth (analz x\<^sub>1))

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> synth (analz x\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth (analz x\<^sub>1))

goal (1 subgoal):
 1. \<forall>x\<^sub>1. x\<^sub>1 \<subseteq> synth (analz x\<^sub>1)
[PROOF STEP]
using F6
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> analz (synth (analz x\<^sub>1))
\<forall>x\<^sub>1. analz (synth (analz x\<^sub>1)) = synth (analz x\<^sub>1)

goal (1 subgoal):
 1. \<forall>x\<^sub>1. x\<^sub>1 \<subseteq> synth (analz x\<^sub>1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> synth (analz x\<^sub>1)

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "H \<subseteq> synth (analz H)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<^sub>1. x\<^sub>1 \<subseteq> synth (analz x\<^sub>1)

goal (1 subgoal):
 1. H \<subseteq> synth (analz H)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
H \<subseteq> synth (analz H)

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> synth (analz H)

goal (1 subgoal):
 1. H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)
[PROOF STEP]
using F5
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> synth (analz H)
X \<in> synth (analz H)

goal (1 subgoal):
 1. H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "insert X H \<subseteq> synth (analz H)"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)

goal (1 subgoal):
 1. insert X H \<subseteq> synth (analz H)
[PROOF STEP]
by (metis insert_subset)
[PROOF STATE]
proof (state)
this:
insert X H \<subseteq> synth (analz H)

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "parts (insert X H) \<subseteq> parts (synth (analz H))"
[PROOF STATE]
proof (prove)
using this:
insert X H \<subseteq> synth (analz H)

goal (1 subgoal):
 1. parts (insert X H) \<subseteq> parts (synth (analz H))
[PROOF STEP]
by (metis parts_mono)
[PROOF STATE]
proof (state)
this:
parts (insert X H) \<subseteq> parts (synth (analz H))

goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H
[PROOF STEP]
hence "parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
[PROOF STATE]
proof (prove)
using this:
parts (insert X H) \<subseteq> parts (synth (analz H))

goal (1 subgoal):
 1. parts (insert X H) \<subseteq> parts H \<union> synth (analz H)
[PROOF STEP]
using F2
[PROOF STATE]
proof (prove)
using this:
parts (insert X H) \<subseteq> parts (synth (analz H))
\<forall>x\<^sub>1. parts x\<^sub>1 \<union> synth (analz x\<^sub>1) = parts (synth (analz x\<^sub>1))

goal (1 subgoal):
 1. parts (insert X H) \<subseteq> parts H \<union> synth (analz H)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
parts (insert X H) \<subseteq> parts H \<union> synth (analz H)

goal (1 subgoal):
 1