[STATEMENT]
lemma varMonotone_byFIX: "Monotone (\<lambda> \<Phi> . (\<lambda> (s,t,\<beta>) .(b,\<Phi>,\<beta>,s,t):var))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotone (\<lambda>\<Phi> (s, t, \<beta>). (b, \<Phi>, \<beta>, s, t) \<in> var)
[PROOF STEP]
apply (subgoal_tac "Monotone (\<lambda> \<Phi> . PhiWhile b \<Phi>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Monotone (PhiWhile b) \<Longrightarrow> Monotone (\<lambda>\<Phi> (s, t, \<beta>). (b, \<Phi>, \<beta>, s, t) \<in> var)
 2. Monotone (PhiWhile b)
[PROOF STEP]
apply (simp add: FIXvarFIX)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotone (PhiWhile b)
[PROOF STEP]
apply (rule PhiWhileMonotone)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done