theory TailrecPre

lemma tailrec_pre_lemma:
  "!f1 g p x. tailrec_pre f1 g p (x::'a) = (p x \<and> (g x \<longrightarrow> tailrec_pre f1 g p (f1 x)))" apply (clarsimp simp add: tailrec_pre_def) apply (rule iffI) apply (rule conjI) apply auto[1] apply clarsimp apply (rule conjI[rotated]) apply (case_tac n) apply simp apply (clarsimp simp: funpow_swap1) apply auto[1] apply clarsimp apply (drule_tac x="Suc n" for n in spec, simp add: funpow_swap1) apply (erule mp) apply clarsimp apply (case_tac m, simp_all add: funpow_swap1)[1] apply (case_tac "g x") apply clarsimp apply (rule conjI) apply clarsimp apply (case_tac k) apply auto[1] apply (simp_all add: funpow_swap1)[1] apply (erule allE, erule impE) prefer 2 apply assumption apply (rule allI) apply (rule impI) apply (drule_tac x="Suc m" in spec, simp_all add: funpow_swap1) apply (rule_tac x="Suc n" in exI) apply (simp add: funpow_swap1) apply (rule conjI) prefer 2 apply (rule_tac x="0" in exI) apply auto[1] apply (rule allI) apply (rule impI) apply (case_tac k) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>f1 g p x. tailrec_pre f1 g p x = (p x \<and> (g x \<longrightarrow> tailrec_pre f1 g p (f1 x))) proof (prove)
goal (1 subgoal):
 1. \<And>f1 g p x. ((\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x))) = (p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x))))) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x. (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) \<Longrightarrow> p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x))))
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x. (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) \<Longrightarrow> p x
 2. \<And>f1 g p x. (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) \<Longrightarrow> g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))
 3. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x. (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) \<Longrightarrow> g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))
 3. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (4 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x; n = 0\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) (f1 x))
 2. \<And>f1 g p x n nat. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) (f1 x))
 3. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))
 4. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n nat. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x; n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))
 3. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x nat. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ nat) (f1 x)); g x\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))
 3. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n k. \<lbrakk>\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x); \<not> g ((f1 ^^ n) x); g x; \<forall>m<k. g ((f1 ^^ m) (f1 x))\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) (f1 x))
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n k. \<lbrakk>\<not> g ((f1 ^^ n) x); g x; \<forall>m<k. g ((f1 ^^ m) (f1 x)); (\<forall>m<Suc (?na51 f1 g p x n k). g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ ?na51 f1 g p x n k) (f1 x))\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) (f1 x))
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n k. \<lbrakk>\<not> g ((f1 ^^ n) x); g x; \<forall>m<k. g ((f1 ^^ m) (f1 x))\<rbrakk> \<Longrightarrow> \<forall>m<Suc k. g ((f1 ^^ m) x)
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g x n k m. \<lbrakk>\<not> g ((f1 ^^ n) x); g x; \<forall>m<k. g ((f1 ^^ m) (f1 x)); m < Suc k\<rbrakk> \<Longrightarrow> g ((f1 ^^ m) x)
 2. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (1 subgoal):
 1. \<And>f1 g p x. p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))) \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x))
 2. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x))
 2. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n k. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<k. g ((f1 ^^ m) x)\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x)
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (4 subgoals):
 1. \<And>f1 g p x n k. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<k. g ((f1 ^^ m) x); k = 0\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x)
 2. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<k. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x)
 3. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 4. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<k. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x)
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> p ((f1 ^^ nat) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (4 subgoals):
 1. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> \<forall>m<?k82 f1 g p x n k nat. g ((f1 ^^ m) (f1 x))
 2. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat; p ((f1 ^^ ?k82 f1 g p x n k nat) (f1 x))\<rbrakk> \<Longrightarrow> p ((f1 ^^ nat) (f1 x))
 3. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 4. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (4 subgoals):
 1. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat; p ((f1 ^^ ?k82 f1 g p x n k nat) (f1 x))\<rbrakk> \<Longrightarrow> p ((f1 ^^ nat) (f1 x))
 2. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> \<forall>m<?k82 f1 g p x n k nat. g ((f1 ^^ m) (f1 x))
 3. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 4. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n k nat. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> \<forall>m<nat. g ((f1 ^^ m) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n k nat m. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> m < nat \<longrightarrow> g ((f1 ^^ m) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (3 subgoals):
 1. \<And>f1 g p x n k nat m. \<lbrakk>g x; p x; \<not> g ((f1 ^^ n) (f1 x)); \<forall>m<Suc nat. g ((f1 ^^ m) x); k = Suc nat; m < nat\<rbrakk> \<Longrightarrow> g ((f1 ^^ m) (f1 x))
 2. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 3. \<And>f1 g p x. \<lbrakk>p x \<and> (g x \<longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x))) \<and> (\<exists>n. \<not> g ((f1 ^^ n) (f1 x)))); \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 2. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x n. \<lbrakk>g x; p x; \<forall>k. (\<forall>m<k. g ((f1 ^^ m) (f1 x))) \<longrightarrow> p ((f1 ^^ k) (f1 x)); \<not> g ((f1 ^^ n) (f1 x))\<rbrakk> \<Longrightarrow> \<not> g ((f1 ^^ Suc n) x)
 2. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (1 subgoal):
 1. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)) \<and> (\<exists>n. \<not> g ((f1 ^^ n) x)) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x)
 2. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<exists>n. \<not> g ((f1 ^^ n) x)
 2. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<not> g ((f1 ^^ 0) x)
 2. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x) proof (prove)
goal (1 subgoal):
 1. \<And>f1 g p x. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> \<forall>k. (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x) proof (prove)
goal (1 subgoal):
 1. \<And>f1 g p x k. \<lbrakk>p x; \<not> g x\<rbrakk> \<Longrightarrow> (\<forall>m<k. g ((f1 ^^ m) x)) \<longrightarrow> p ((f1 ^^ k) x) proof (prove)
goal (1 subgoal):
 1. \<And>f1 g p x k. \<lbrakk>p x; \<not> g x; \<forall>m<k. g ((f1 ^^ m) x)\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x) proof (prove)
goal (2 subgoals):
 1. \<And>f1 g p x k. \<lbrakk>p x; \<not> g x; \<forall>m<k. g ((f1 ^^ m) x); k = 0\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x)
 2. \<And>f1 g p x k nat. \<lbrakk>p x; \<not> g x; \<forall>m<k. g ((f1 ^^ m) x); k = Suc nat\<rbrakk> \<Longrightarrow> p ((f1 ^^ k) x) proof (prove)
goal:
No subgoals!