[STATEMENT]
lemma (in Group) joint_D_gchains:"\<lbrakk>D_gchain G n f; D_gchain G m g; 
       g 0 \<subset> f n \<rbrakk> \<Longrightarrow>  D_gchain G (Suc (n + m)) (jointfun n f m g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> D_gchain G (Suc (n + m)) (jointfun n f m g)
[PROOF STEP]
apply (simp add:D_gchain_def [of "G" "Suc (n + m)" _])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> d_gchain G (Suc (n + m)) (jointfun n f m g) \<and> (\<forall>l\<le>n + m. jointfun n f m g (Suc l) \<subset> jointfun n f m g l)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> d_gchain G (Suc (n + m)) (jointfun n f m g)
 2. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> \<forall>l\<le>n + m. jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (rule joint_d_gchains[of n f m g],
       simp add:D_gchain_is_d_gchain,
       simp add:D_gchain_is_d_gchain,
       simp add:psubset_imp_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> \<forall>l\<le>n + m. jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (case_tac "Suc l \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (simp add:jointfun_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> f (Suc l) \<subset> f l
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (rule_tac i = l and j = "Suc l" in D_gchain0[of n f], assumption,
        cut_tac x = l and y = "Suc l" and z = n in less_le_trans)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> l < Suc l
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> Suc l \<le> n
 3. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n; l < n\<rbrakk> \<Longrightarrow> l \<le> n
 4. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> Suc l \<le> n
 5. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> l < Suc l
 6. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (simp add:nat_not_le_less,
        frule_tac m = n and n = "Suc l" in Suc_leI, thin_tac "n < Suc l", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n \<le> l\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (case_tac "l = n", simp add:jointfun_def sliden_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n \<le> l; l \<noteq> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (frule not_sym, thin_tac "l \<noteq> n",
        frule_tac x = n and y = l in le_imp_less_or_eq,
        thin_tac "n \<le> l", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (simp add:jointfun_def sliden_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l\<rbrakk> \<Longrightarrow> g (l - n) \<subset> g (l - Suc n)
[PROOF STEP]
apply (frule_tac m = l and n = "n + m" and l = n in  diff_le_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> n + m - n\<rbrakk> \<Longrightarrow> g (l - n) \<subset> g (l - Suc n)
[PROOF STEP]
apply (simp add:diff_add_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> g (l - n) \<subset> g (l - Suc n)
[PROOF STEP]
apply (rule_tac i = "l - Suc n" and j = "l - n" in D_gchain0[of m g],
         assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> l - Suc n \<le> m
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> l - n \<le> m
 3. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> l - Suc n < l - n
[PROOF STEP]
apply (arith, assumption, arith)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done