[STATEMENT]
lemma pass_ATC_io_fail :
  assumes "\<not>pass_ATC M A FS"
  and     "is_ATC A"
  and     "observable M"
  and     "(inputs A) \<subseteq> (inputs M)"
shows "initial A \<in> FS \<or> (\<exists> io ioA ioM . io@[ioA] \<in> L A
                          \<and> io@[ioM] \<in> L M
                          \<and> fst ioA = fst ioM
                          \<and> (io@[ioM] \<notin> L A \<or> io_targets A (io@[ioM]) (initial A) \<inter> FS \<noteq> {}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial A \<in> FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> FS \<noteq> {}))
[PROOF STEP]
using pass_ATC'_io_fail[OF _ assms(2-4)]
[PROOF STATE]
proof (prove)
using this:
\<not> pass_ATC' M A ?FS ?k \<Longrightarrow> FSM.initial A \<in> ?FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> ?FS \<noteq> {}))

goal (1 subgoal):
 1. FSM.initial A \<in> FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> FS \<noteq> {}))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> pass_ATC' M A ?FS ?k \<Longrightarrow> FSM.initial A \<in> ?FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> ?FS \<noteq> {}))
\<not> pass_ATC M A FS

goal (1 subgoal):
 1. FSM.initial A \<in> FS \<or> (\<exists>io ioA ioM. io @ [ioA] \<in> L A \<and> io @ [ioM] \<in> L M \<and> fst ioA = fst ioM \<and> (io @ [ioM] \<notin> L A \<or> io_targets A (io @ [ioM]) (FSM.initial A) \<inter> FS \<noteq> {}))
[PROOF STEP]
by auto