[STATEMENT]
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
          (if A\<in>bad then insert X (spies evs) else spies evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows Spy (evs @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy evs) else knows Spy evs)
[PROOF STEP]
apply (induct_tac "evs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. knows Spy ([] @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy []) else knows Spy [])
 2. \<And>a list. knows Spy (list @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy list) else knows Spy list) \<Longrightarrow> knows Spy ((a # list) @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy (a # list)) else knows Spy (a # list))
[PROOF STEP]
apply (rename_tac [2] a b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. knows Spy ([] @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy []) else knows Spy [])
 2. \<And>a b. knows Spy (b @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy b) else knows Spy b) \<Longrightarrow> knows Spy ((a # b) @ [Notes A X]) = (if A \<in> bad then insert X (knows Spy (a # b)) else knows Spy (a # b))
[PROOF STEP]
apply (induct_tac [2] "a", auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done