[STATEMENT]
lemma HierAuto_EmptySet:
 "((@x. True),{Abs_seqauto ({@x. True}, (@x. True), {}, {})}, {}, 
  Map.empty ( @x. True \<mapsto> {})) \<in> {(D,F,E,G) | D F E G. HierAuto D F E G}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. True, {Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})}, {}, [SOME x. True \<mapsto> {}]) \<in> {(D, F, E, G) |D F E G. HierAuto D F E G}
[PROOF STEP]
apply (unfold HierAuto_def IsCompFun_def Root_def RootEx_def MutuallyDistinct_def
           OneAncestor_def NoCycles_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. True, {Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})}, {}, [SOME x. True \<mapsto> {}]) \<in> {(D, F, E, G) |D F E G. \<Union> (SAEvents ` F) \<subseteq> E \<and> (\<forall>a\<in>F. \<forall>b\<in>F. a \<noteq> b \<longrightarrow> States a \<inter> States b = {}) \<and> finite F \<and> dom G = \<Union> (States ` F) \<and> \<Union> (ran G) = F - {SOME A. A \<in> F \<and> A \<notin> \<Union> (ran G)} \<and> (\<exists>!A. A \<in> F \<and> A \<notin> \<Union> (ran G)) \<and> (\<forall>A\<in>F - {SOME A. A \<in> F \<and> A \<notin> \<Union> (ran G)}. \<exists>!s. s \<in> \<Union> (States ` (F - {A})) \<and> A \<in> the (G s)) \<and> (\<forall>S\<in>Pow (\<Union> (States ` F)). S \<noteq> {} \<longrightarrow> (\<exists>s\<in>S. S \<inter> \<Union> (States ` the (G s)) = {}))}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done