theory ListLibLemmas

lemma range_nat_relation_induct:
"\<lbrakk> m = Suc (n + k) ; m < cap ; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n );
   \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k \<rbrakk> \<Longrightarrow>  P n m" apply (clarify) apply (thin_tac "m = t" for t) apply (induct k) apply (drule_tac x = "n" in spec) apply (erule impE, simp, simp) apply (frule_tac x = "Suc (n + k)" in spec) apply (erule impE) apply (simp only: add_Suc_right) apply (rotate_tac 3, frule_tac x = n in spec) apply (rotate_tac -1, drule_tac x = "Suc (n + k)" in spec) apply (rotate_tac -1, drule_tac x = "Suc (n + Suc k) " in spec) apply (erule impE) apply (intro conjI) apply (rule_tac y = "Suc (n + Suc k)" in less_trans) apply (rule less_SucI) apply (simp only: add_Suc_right)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = Suc (n + k); m < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; m = Suc (n + k)\<rbrakk> \<Longrightarrow> P n (Suc (n + k)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (n + 0) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + 0))
 2. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (n + 0) < cap; \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> P n (Suc (n + 0))
 2. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; Suc (Suc (n + k)) < cap \<longrightarrow> P (Suc (n + k)) (Suc (Suc (n + k)))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> Suc (Suc (n + k)) < cap
 2. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k)))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k)))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>j k. n < cap \<and> j < cap \<and> k < cap \<longrightarrow> P n j \<longrightarrow> P j k \<longrightarrow> P n k\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>ka. n < cap \<and> Suc (n + k) < cap \<and> ka < cap \<longrightarrow> P n (Suc (n + k)) \<longrightarrow> P (Suc (n + k)) ka \<longrightarrow> P n ka\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); n < cap \<and> Suc (n + k) < cap \<and> Suc (n + Suc k) < cap \<longrightarrow> P n (Suc (n + k)) \<longrightarrow> P (Suc (n + k)) (Suc (n + Suc k)) \<longrightarrow> P n (Suc (n + Suc k))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> n < cap \<and> Suc (n + k) < cap \<and> Suc (n + Suc k) < cap
 2. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); P n (Suc (n + k)) \<longrightarrow> P (Suc (n + k)) (Suc (n + Suc k)) \<longrightarrow> P n (Suc (n + Suc k))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (4 subgoals):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> n < cap
 2. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + k) < cap
 3. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + Suc k) < cap
 4. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); P n (Suc (n + k)) \<longrightarrow> P (Suc (n + k)) (Suc (n + Suc k)) \<longrightarrow> P n (Suc (n + Suc k))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (5 subgoals):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> n < Suc (n + Suc k)
 2. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + Suc k) < cap
 3. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + k) < cap
 4. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + Suc k) < cap
 5. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); P n (Suc (n + k)) \<longrightarrow> P (Suc (n + k)) (Suc (n + Suc k)) \<longrightarrow> P n (Suc (n + Suc k))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal (5 subgoals):
 1. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> n < n + Suc k
 2. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + Suc k) < cap
 3. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + k) < cap
 4. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n)\<rbrakk> \<Longrightarrow> Suc (n + Suc k) < cap
 5. \<And>k. \<lbrakk>\<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k; P (Suc (n + k)) (Suc (Suc (n + k))); \<lbrakk>Suc (n + k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); \<forall>i j k. i < cap \<and> j < cap \<and> k < cap \<longrightarrow> P i j \<longrightarrow> P j k \<longrightarrow> P i k\<rbrakk> \<Longrightarrow> P n (Suc (n + k)); Suc (n + Suc k) < cap; \<forall>n. Suc n < cap \<longrightarrow> P n (Suc n); P n (Suc (n + k)) \<longrightarrow> P (Suc (n + k)) (Suc (n + Suc k)) \<longrightarrow> P n (Suc (n + Suc k))\<rbrakk> \<Longrightarrow> P n (Suc (n + Suc k)) proof (prove)
goal:
No subgoals!