[STATEMENT]
lemma resolution_example2:
   "resolution_deriv {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
                              {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
have "resolution_step
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}} \<union> {{Na,Pb}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} \<union> {{Na, Pb}})
[PROOF STEP]
apply (rule resolution_rule'[of "{Pax}" _ "{Na,Pb,Naa}" "{Pax}" "{Naa}" mguPaaPax ])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Pax} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}}
 2. {Na, Pb, Naa} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}}
 3. applicable {Pax} {Na, Pb, Naa} {Pax} {Naa} mguPaaPax
 4. {{Na, Pb}} = {resolution {Pax} {Na, Pb, Naa} {Pax} {Naa} mguPaaPax}
[PROOF STEP]
using mguPaaPax_mgu
[PROOF STATE]
proof (prove)
using this:
mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}

goal (4 subgoals):
 1. {Pax} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}}
 2. {Na, Pb, Naa} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}}
 3. applicable {Pax} {Na, Pb, Naa} {Pax} {Naa} mguPaaPax
 4. {{Na, Pb}} = {resolution {Pax} {Na, Pb, Naa} {Pax} {Naa} mguPaaPax}
[PROOF STEP]
unfolding applicable_def vars\<^sub>l\<^sub>s_def  vars\<^sub>l_def
          Nb_def Na_def Pax_def Pa_def Pb_def Naa_def Paa_def mguPaaPax_def resolution_def
[PROOF STATE]
proof (prove)
using this:
mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']}

goal (4 subgoals):
 1. {Pos ''a'' [\<epsilon> ''x'']} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pos ''a'' [\<epsilon> ''x'']}, {Pos ''a'' []}, {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]}}
 2. {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pos ''a'' [\<epsilon> ''x'']}, {Pos ''a'' []}, {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]}}
 3. {Pos ''a'' [\<epsilon> ''x'']} \<noteq> {} \<and> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} \<noteq> {} \<and> {Pos ''a'' [\<epsilon> ''x'']} \<noteq> {} \<and> {Neg ''a'' [Fun ''a'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Pos ''a'' [\<epsilon> ''x'']}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Pos ''a'' [\<epsilon> ''x'']} \<subseteq> {Pos ''a'' [\<epsilon> ''x'']} \<and> {Neg ''a'' [Fun ''a'' []]} \<subseteq> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} \<and> mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) ({Pos ''a'' [\<epsilon> ''x'']} \<union> {Neg ''a'' [Fun ''a'' []]}\<^sup>C)
 4. {{Neg ''a'' [], Pos ''b'' []}} = {{Pos ''a'' [\<epsilon> ''x'']} - {Pos ''a'' [\<epsilon> ''x'']} \<union> ({Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]}) \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Neg ''a'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]} \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
 2. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]} \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
[PROOF STEP]
apply (rule_tac x=Na in image_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Neg ''a'' [] = Na \<cdot>\<^sub>l (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
 2. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Na \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]}
 3. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]} \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
[PROOF STEP]
unfolding Na_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Neg ''a'' [] = Neg ''a'' [] \<cdot>\<^sub>l (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
 2. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Neg ''a'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]}
 3. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]} \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]} \<cdot>\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
[PROOF STEP]
apply (rule_tac x=Pb in image_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] = Pb \<cdot>\<^sub>l (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
 2. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pb \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]}
[PROOF STEP]
unfolding Pb_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] = Pos ''b'' [] \<cdot>\<^sub>l (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x)
 2. mgu\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']} \<Longrightarrow> Pos ''b'' [] \<in> {Neg ''a'' [], Pos ''b'' [], Neg ''a'' [Fun ''a'' []]} - {Neg ''a'' [Fun ''a'' []]}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} \<union> {{Na, Pb}})

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} \<union> {{Na, Pb}})
[PROOF STEP]
have "resolution_step
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}})"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} \<union> {{Na, Pb}})

goal (1 subgoal):
 1. resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
have "resolution_step
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}} \<union> {{Na}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} \<union> {{Na}})
[PROOF STEP]
apply (rule resolution_rule'[of "{Nb,Na}" _ "{Na,Pb}" "{Nb}" "{Pb}" \<epsilon>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Nb, Na} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}
 2. {Na, Pb} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}
 3. applicable {Nb, Na} {Na, Pb} {Nb} {Pb} \<epsilon>
 4. {{Na}} = {resolution {Nb, Na} {Na, Pb} {Nb} {Pb} \<epsilon>}
[PROOF STEP]
unfolding applicable_def vars\<^sub>l\<^sub>s_def  vars\<^sub>l_def
                 Pb_def Nb_def Na_def PP_def resolution_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Neg ''b'' [], Neg ''a'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pa}, {Neg ''a'' [], Pos ''b'' [], Naa}, {Neg ''a'' [], Pos ''b'' []}}
 2. {Neg ''a'' [], Pos ''b'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pa}, {Neg ''a'' [], Pos ''b'' [], Naa}, {Neg ''a'' [], Pos ''b'' []}}
 3. {Neg ''b'' [], Neg ''a'' []} \<noteq> {} \<and> {Neg ''a'' [], Pos ''b'' []} \<noteq> {} \<and> {Neg ''b'' []} \<noteq> {} \<and> {Pos ''b'' []} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''b'' [], Neg ''a'' []}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Neg ''a'' [], Pos ''b'' []}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''b'' []} \<subseteq> {Neg ''b'' [], Neg ''a'' []} \<and> {Pos ''b'' []} \<subseteq> {Neg ''a'' [], Pos ''b'' []} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''b'' []} \<union> {Pos ''b'' []}\<^sup>C)
 4. {{Neg ''a'' []}} = {{Neg ''b'' [], Neg ''a'' []} - {Neg ''b'' []} \<union> ({Neg ''a'' [], Pos ''b'' []} - {Pos ''b'' []}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
using unifier_single empty_mgu
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s ?\<sigma> {?l}
unifier\<^sub>l\<^sub>s \<epsilon> ?L \<Longrightarrow> mgu\<^sub>l\<^sub>s \<epsilon> ?L

goal (4 subgoals):
 1. {Neg ''b'' [], Neg ''a'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pa}, {Neg ''a'' [], Pos ''b'' [], Naa}, {Neg ''a'' [], Pos ''b'' []}}
 2. {Neg ''a'' [], Pos ''b'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pa}, {Neg ''a'' [], Pos ''b'' [], Naa}, {Neg ''a'' [], Pos ''b'' []}}
 3. {Neg ''b'' [], Neg ''a'' []} \<noteq> {} \<and> {Neg ''a'' [], Pos ''b'' []} \<noteq> {} \<and> {Neg ''b'' []} \<noteq> {} \<and> {Pos ''b'' []} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''b'' [], Neg ''a'' []}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Neg ''a'' [], Pos ''b'' []}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''b'' []} \<subseteq> {Neg ''b'' [], Neg ''a'' []} \<and> {Pos ''b'' []} \<subseteq> {Neg ''a'' [], Pos ''b'' []} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''b'' []} \<union> {Pos ''b'' []}\<^sup>C)
 4. {{Neg ''a'' []}} = {{Neg ''b'' [], Neg ''a'' []} - {Neg ''b'' []} \<union> ({Neg ''a'' [], Pos ''b'' []} - {Pos ''b'' []}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} \<union> {{Na}})

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} \<union> {{Na}})
[PROOF STEP]
have "resolution_step
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}})"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} \<union> {{Na}})

goal (1 subgoal):
 1. resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
have "resolution_step
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}} \<union> {{}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} \<union> {{}})
[PROOF STEP]
apply (rule resolution_rule'[of "{Na}" _ "{Pa}" "{Na}" "{Pa}" \<epsilon>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Na} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}
 2. {Pa} \<in> {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}
 3. applicable {Na} {Pa} {Na} {Pa} \<epsilon>
 4. {{}} = {resolution {Na} {Pa} {Na} {Pa} \<epsilon>}
[PROOF STEP]
unfolding applicable_def vars\<^sub>l\<^sub>s_def  vars\<^sub>l_def
                  Pa_def Nb_def Na_def PP_def resolution_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Neg ''a'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pos ''a'' []}, {Neg ''a'' [], Pb, Naa}, {Neg ''a'' [], Pb}, {Neg ''a'' []}}
 2. {Pos ''a'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pos ''a'' []}, {Neg ''a'' [], Pb, Naa}, {Neg ''a'' [], Pb}, {Neg ''a'' []}}
 3. {Neg ''a'' []} \<noteq> {} \<and> {Pos ''a'' []} \<noteq> {} \<and> {Neg ''a'' []} \<noteq> {} \<and> {Pos ''a'' []} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''a'' []}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Pos ''a'' []}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''a'' []} \<subseteq> {Neg ''a'' []} \<and> {Pos ''a'' []} \<subseteq> {Pos ''a'' []} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''a'' []} \<union> {Pos ''a'' []}\<^sup>C)
 4. {{}} = {{Neg ''a'' []} - {Neg ''a'' []} \<union> ({Pos ''a'' []} - {Pos ''a'' []}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
using unifier_single empty_mgu
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s ?\<sigma> {?l}
unifier\<^sub>l\<^sub>s \<epsilon> ?L \<Longrightarrow> mgu\<^sub>l\<^sub>s \<epsilon> ?L

goal (4 subgoals):
 1. {Neg ''a'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pos ''a'' []}, {Neg ''a'' [], Pb, Naa}, {Neg ''a'' [], Pb}, {Neg ''a'' []}}
 2. {Pos ''a'' []} \<in> {{Neg ''b'' [], Neg ''a'' []}, {Pax}, {Pos ''a'' []}, {Neg ''a'' [], Pb, Naa}, {Neg ''a'' [], Pb}, {Neg ''a'' []}}
 3. {Neg ''a'' []} \<noteq> {} \<and> {Pos ''a'' []} \<noteq> {} \<and> {Neg ''a'' []} \<noteq> {} \<and> {Pos ''a'' []} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''a'' []}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Pos ''a'' []}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''a'' []} \<subseteq> {Neg ''a'' []} \<and> {Pos ''a'' []} \<subseteq> {Pos ''a'' []} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''a'' []} \<union> {Pos ''a'' []}\<^sup>C)
 4. {{}} = {{Neg ''a'' []} - {Neg ''a'' []} \<union> ({Pos ''a'' []} - {Pos ''a'' []}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} \<union> {{}})

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} \<union> {{}})
[PROOF STEP]
have "resolution_step
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na}}
         ({{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}})"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} ({{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} \<union> {{}})

goal (1 subgoal):
 1. resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
have "resolution_deriv {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}
          {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa},{Na,Pb},{Na},{}}"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
unfolding resolution_deriv_def
[PROOF STATE]
proof (prove)
using this:
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}}
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}}
resolution_step {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}

goal (1 subgoal):
 1. resolution_step\<^sup>*\<^sup>* {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}

goal (1 subgoal):
 1. resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resolution_example1_sem: "\<not>eval\<^sub>c\<^sub>s F G {{NP, PQ}, {NQ}, {PP, PQ}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G {{NP, PQ}, {NQ}, {PP, PQ}}
[PROOF STEP]
using resolution_example1 derivation_sound_refute
[PROOF STATE]
proof (prove)
using this:
resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
resolution_deriv ?Cs ?Cs' \<and> {} \<in> ?Cs' \<Longrightarrow> \<not> eval\<^sub>c\<^sub>s ?F ?G ?Cs

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G {{NP, PQ}, {NQ}, {PP, PQ}}
[PROOF STEP]
by auto


[STATEMENT]
lemma resolution_example2_sem: "\<not>eval\<^sub>c\<^sub>s F G {{Nb,Na},{Pax},{Pa},{Na,Pb,Naa}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}}
[PROOF STEP]
using resolution_example2 derivation_sound_refute
[PROOF STATE]
proof (prove)
using this:
resolution_deriv {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}} {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}, {Na, Pb}, {Na}, {}}
resolution_deriv ?Cs ?Cs' \<and> {} \<in> ?Cs' \<Longrightarrow> \<not> eval\<^sub>c\<^sub>s ?F ?G ?Cs

goal (1 subgoal):
 1. \<not> eval\<^sub>c\<^sub>s F G {{Nb, Na}, {Pax}, {Pa}, {Na, Pb, Naa}}
[PROOF STEP]
by auto


[STATEMENT]
lemma quasiconvexD:
  assumes "quasiconvex C X" "x \<in> X" "y \<in> X"
  shows "\<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quasiconvex C X
x \<in> X
y \<in> X

goal (1 subgoal):
 1. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C)
[PROOF STEP]
unfolding quasiconvex_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C))
x \<in> X
y \<in> X

goal (1 subgoal):
 1. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C)
[PROOF STEP]
by auto


[STATEMENT]
lemma quasiconvexC:
  assumes "quasiconvex C X"
  shows "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
quasiconvex C X

goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
unfolding quasiconvex_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C))

goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
by auto


[STATEMENT]
lemma quasiconvexI:
  assumes "C \<ge> 0"
          "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> (\<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C))"
  shows "quasiconvex C X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasiconvex C X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G ?x ?y \<and> (\<forall>z\<in>G. infdist z X \<le> C)

goal (1 subgoal):
 1. quasiconvex C X
[PROOF STEP]
unfolding quasiconvex_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G ?x ?y \<and> (\<forall>z\<in>G. infdist z X \<le> C)

goal (1 subgoal):
 1. 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z X \<le> C))
[PROOF STEP]
by auto


[STATEMENT]
lemma quasiconvex_of_geodesic:
  assumes "geodesic_segment G"
  shows "quasiconvex 0 G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasiconvex 0 G
[PROOF STEP]
proof (rule quasiconvexI, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> G; y \<in> G\<rbrakk> \<Longrightarrow> \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> 0)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> G; y \<in> G\<rbrakk> \<Longrightarrow> \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> 0)
[PROOF STEP]
assume *: "x \<in> G" "y \<in> G"
[PROOF STATE]
proof (state)
this:
x \<in> G
y \<in> G

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> G; y \<in> G\<rbrakk> \<Longrightarrow> \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> 0)
[PROOF STEP]
obtain H where H: "H \<subseteq> G" "geodesic_segment_between H x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>H. \<lbrakk>H \<subseteq> G; geodesic_segment_between H x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using geodesic_subsegment_exists[OF assms(1) *]
[PROOF STATE]
proof (prove)
using this:
\<exists>H\<subseteq>G. geodesic_segment_between H x y

goal (1 subgoal):
 1. (\<And>H. \<lbrakk>H \<subseteq> G; geodesic_segment_between H x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H \<subseteq> G
geodesic_segment_between H x y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> G; y \<in> G\<rbrakk> \<Longrightarrow> \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> 0)
[PROOF STEP]
have "infdist z G \<le> 0" if "z \<in> H" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist z G \<le> 0
[PROOF STEP]
using H(1) that
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> G
z \<in> H

goal (1 subgoal):
 1. infdist z G \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?z \<in> H \<Longrightarrow> infdist ?z G \<le> 0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> G; y \<in> G\<rbrakk> \<Longrightarrow> \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?z \<in> H \<Longrightarrow> infdist ?z G \<le> 0
[PROOF STEP]
show "\<exists>H. geodesic_segment_between H x y \<and> (\<forall>z\<in>H. infdist z G \<le> 0)"
[PROOF STATE]
proof (prove)
using this:
?z \<in> H \<Longrightarrow> infdist ?z G \<le> 0

goal (1 subgoal):
 1. \<exists>H. geodesic_segment_between H x y \<and> (\<forall>z\<in>H. infdist z G \<le> 0)
[PROOF STEP]
using H(2)
[PROOF STATE]
proof (prove)
using this:
?z \<in> H \<Longrightarrow> infdist ?z G \<le> 0
geodesic_segment_between H x y

goal (1 subgoal):
 1. \<exists>H. geodesic_segment_between H x y \<and> (\<forall>z\<in>H. infdist z G \<le> 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>H. geodesic_segment_between H x y \<and> (\<forall>z\<in>H. infdist z G \<le> 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasiconvex_empty:
  assumes "C \<ge> 0"
  shows "quasiconvex C {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasiconvex C {}
[PROOF STEP]
unfolding quasiconvex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C \<and> (\<forall>x\<in>{}. \<forall>y\<in>{}. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z {} \<le> C))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> C \<and> (\<forall>x\<in>{}. \<forall>y\<in>{}. \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z {} \<le> C))
[PROOF STEP]
by auto


[STATEMENT]
lemma quasiconvex_mono:
  assumes "C \<le> D"
          "quasiconvex C G"
  shows "quasiconvex D G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasiconvex D G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> D
quasiconvex C G

goal (1 subgoal):
 1. quasiconvex D G
[PROOF STEP]
unfolding quasiconvex_def
[PROOF STATE]
proof (prove)
using this:
C \<le> D
0 \<le> C \<and> (\<forall>x\<in>G. \<forall>y\<in>G. \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> C))

goal (1 subgoal):
 1. 0 \<le> D \<and> (\<forall>x\<in>G. \<forall>y\<in>G. \<exists>Ga. geodesic_segment_between Ga x y \<and> (\<forall>z\<in>Ga. infdist z G \<le> D))
[PROOF STEP]
by (auto, fastforce)


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) quasiconvex_thickening:
  assumes "quasiconvex C (X::'a set)" "r \<ge> 0"
  shows "quasiconvex (C + 8 *deltaG(TYPE('a))) (\<Union>x\<in>X. cball x r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasiconvex (C + 8 * deltaG TYPE('a)) (\<Union>x\<in>X. cball x r)
[PROOF STEP]
proof (rule quasiconvexI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> C + 8 * deltaG TYPE('a)
 2. \<And>x y. \<lbrakk>x \<in> (\<Union>x\<in>X. cball x r); y \<in> (\<Union>x\<in>X. cball x r)\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
show "C + 8 *deltaG(TYPE('a)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
using quasiconvexC[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> C + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (\<Union>x\<in>X. cball x r); y \<in> (\<Union>x\<in>X. cball x r)\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (\<Union>x\<in>X. cball x r); y \<in> (\<Union>x\<in>X. cball x r)\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
fix y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (\<Union>x\<in>X. cball x r); y \<in> (\<Union>x\<in>X. cball x r)\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
assume *: "y \<in> (\<Union>x\<in>X. cball x r)" "z \<in> (\<Union>x\<in>X. cball x r)"
[PROOF STATE]
proof (state)
this:
y \<in> (\<Union>x\<in>X. cball x r)
z \<in> (\<Union>x\<in>X. cball x r)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (\<Union>x\<in>X. cball x r); y \<in> (\<Union>x\<in>X. cball x r)\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
have A: "infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)" if "w \<in> {y--z}" for w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
obtain py where py: "py \<in> X" "y \<in> cball py r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>py. \<lbrakk>py \<in> X; y \<in> cball py r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
y \<in> (\<Union>x\<in>X. cball x r)
z \<in> (\<Union>x\<in>X. cball x r)

goal (1 subgoal):
 1. (\<And>py. \<lbrakk>py \<in> X; y \<in> cball py r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
py \<in> X
y \<in> cball py r

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
obtain pz where pz: "pz \<in> X" "z \<in> cball pz r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pz. \<lbrakk>pz \<in> X; z \<in> cball pz r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
y \<in> (\<Union>x\<in>X. cball x r)
z \<in> (\<Union>x\<in>X. cball x r)

goal (1 subgoal):
 1. (\<And>pz. \<lbrakk>pz \<in> X; z \<in> cball pz r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pz \<in> X
z \<in> cball pz r

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
obtain G where G: "geodesic_segment_between G py pz" "(\<forall>p\<in>G. infdist p X \<le> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>G. \<lbrakk>geodesic_segment_between G py pz; \<forall>p\<in>G. infdist p X \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quasiconvexD[OF assms(1) \<open>py \<in> X\<close> \<open>pz \<in> X\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G py pz \<and> (\<forall>z\<in>G. infdist z X \<le> C)

goal (1 subgoal):
 1. (\<And>G. \<lbrakk>geodesic_segment_between G py pz; \<forall>p\<in>G. infdist p X \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G py pz
\<forall>p\<in>G. infdist p X \<le> C

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
have A: "infdist w ({y--py} \<union> G \<union> {pz--z}) \<le> 8 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w ({y--py} \<union> G \<union> {pz--z}) \<le> 8 * deltaG TYPE('a)
[PROOF STEP]
by (rule thin_quadrilaterals[OF _ G(1) _ _ \<open>w \<in> {y--z}\<close>, where ?x = y and ?t = z], auto)
[PROOF STATE]
proof (state)
this:
infdist w ({y--py} \<union> G \<union> {pz--z}) \<le> 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
have "\<exists>u \<in> {y--py} \<union> G \<union> {pz--z}. infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u\<in>{y--py} \<union> G \<union> {pz--z}. infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u
[PROOF STEP]
apply (rule infdist_proper_attained, auto intro!: proper_Un simp add: geodesic_segment_topology(7))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper G
[PROOF STEP]
by (meson G(1) geodesic_segmentI geodesic_segment_topology(7))
[PROOF STATE]
proof (state)
this:
\<exists>u\<in>{y--py} \<union> G \<union> {pz--z}. infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u\<in>{y--py} \<union> G \<union> {pz--z}. infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u
[PROOF STEP]
obtain u where u: "u \<in> {y--py} \<union> G \<union> {pz--z}" "infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u"
[PROOF STATE]
proof (prove)
using this:
\<exists>u\<in>{y--py} \<union> G \<union> {pz--z}. infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> {y--py} \<union> G \<union> {pz--z}; infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> {y--py} \<union> G \<union> {pz--z}
infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> {y--py} \<union> G \<union> {pz--z}
infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u
[PROOF STEP]
consider "u \<in> {y--py}" | "u \<in> G" | "u \<in> {pz--z}"
[PROOF STATE]
proof (prove)
using this:
u \<in> {y--py} \<union> G \<union> {pz--z}
infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u

goal (1 subgoal):
 1. \<lbrakk>u \<in> {y--py} \<Longrightarrow> thesis; u \<in> G \<Longrightarrow> thesis; u \<in> {pz--z} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>u \<in> {y--py} \<Longrightarrow> ?thesis; u \<in> G \<Longrightarrow> ?thesis; u \<in> {pz--z} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>u \<in> {y--py} \<Longrightarrow> ?thesis; u \<in> G \<Longrightarrow> ?thesis; u \<in> {pz--z} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have "infdist u (\<Union>x\<in>X. cball x r) \<le> C"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<in> {y--py} \<Longrightarrow> ?thesis; u \<in> G \<Longrightarrow> ?thesis; u \<in> {pz--z} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
u \<in> {y--py}

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> {y--py}
[PROOF STEP]
have "dist py u \<le> dist py y"
[PROOF STATE]
proof (prove)
using this:
u \<in> {y--py}

goal (1 subgoal):
 1. dist py u \<le> dist py y
[PROOF STEP]
using geodesic_segment_dist_le local.some_geodesic_is_geodesic_segment(1) some_geodesic_commute some_geodesic_endpoints(1)
[PROOF STATE]
proof (prove)
using this:
u \<in> {y--py}
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G; ?b \<in> ?G\<rbrakk> \<Longrightarrow> dist ?a ?b \<le> dist ?x ?y
geodesic_segment_between {?x--?y} ?x ?y
{?x--?S--?y} = {?y--?S--?x}
?x \<in> {?x--?S--?y}

goal (1 subgoal):
 1. dist py u \<le> dist py y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist py u \<le> dist py y

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist py u \<le> dist py y

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
have "... \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py y \<le> r
[PROOF STEP]
using py(2)
[PROOF STATE]
proof (prove)
using this:
y \<in> cball py r

goal (1 subgoal):
 1. dist py y \<le> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist py y \<le> r

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist py u \<le> r
[PROOF STEP]
have "u \<in> cball py r"
[PROOF STATE]
proof (prove)
using this:
dist py u \<le> r

goal (1 subgoal):
 1. u \<in> cball py r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> cball py r

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> cball py r
[PROOF STEP]
have "u \<in> (\<Union>x\<in>X. cball x r)"
[PROOF STATE]
proof (prove)
using this:
u \<in> cball py r

goal (1 subgoal):
 1. u \<in> (\<Union>x\<in>X. cball x r)
[PROOF STEP]
using py(1)
[PROOF STATE]
proof (prove)
using this:
u \<in> cball py r
py \<in> X

goal (1 subgoal):
 1. u \<in> (\<Union>x\<in>X. cball x r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> (\<Union>x\<in>X. cball x r)

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> (\<Union>x\<in>X. cball x r)
[PROOF STEP]
have "infdist u (\<Union>x\<in>X. cball x r) = 0"
[PROOF STATE]
proof (prove)
using this:
u \<in> (\<Union>x\<in>X. cball x r)

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) = 0

goal (3 subgoals):
 1. u \<in> {y--py} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 3. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infdist u (\<Union>x\<in>X. cball x r) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) = 0

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
using quasiconvexC[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) = 0
0 \<le> C

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
u \<in> {pz--z}

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> {pz--z}
[PROOF STEP]
have "dist pz u \<le> dist pz z"
[PROOF STATE]
proof (prove)
using this:
u \<in> {pz--z}

goal (1 subgoal):
 1. dist pz u \<le> dist pz z
[PROOF STEP]
using geodesic_segment_dist_le local.some_geodesic_is_geodesic_segment(1) some_geodesic_commute some_geodesic_endpoints(1)
[PROOF STATE]
proof (prove)
using this:
u \<in> {pz--z}
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G; ?b \<in> ?G\<rbrakk> \<Longrightarrow> dist ?a ?b \<le> dist ?x ?y
geodesic_segment_between {?x--?y} ?x ?y
{?x--?S--?y} = {?y--?S--?x}
?x \<in> {?x--?S--?y}

goal (1 subgoal):
 1. dist pz u \<le> dist pz z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist pz u \<le> dist pz z

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist pz u \<le> dist pz z

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
have "... \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pz z \<le> r
[PROOF STEP]
using pz(2)
[PROOF STATE]
proof (prove)
using this:
z \<in> cball pz r

goal (1 subgoal):
 1. dist pz z \<le> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist pz z \<le> r

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist pz u \<le> r
[PROOF STEP]
have "u \<in> cball pz r"
[PROOF STATE]
proof (prove)
using this:
dist pz u \<le> r

goal (1 subgoal):
 1. u \<in> cball pz r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> cball pz r

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> cball pz r
[PROOF STEP]
have "u \<in> (\<Union>x\<in>X. cball x r)"
[PROOF STATE]
proof (prove)
using this:
u \<in> cball pz r

goal (1 subgoal):
 1. u \<in> (\<Union>x\<in>X. cball x r)
[PROOF STEP]
using pz(1)
[PROOF STATE]
proof (prove)
using this:
u \<in> cball pz r
pz \<in> X

goal (1 subgoal):
 1. u \<in> (\<Union>x\<in>X. cball x r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> (\<Union>x\<in>X. cball x r)

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> (\<Union>x\<in>X. cball x r)
[PROOF STEP]
have "infdist u (\<Union>x\<in>X. cball x r) = 0"
[PROOF STATE]
proof (prove)
using this:
u \<in> (\<Union>x\<in>X. cball x r)

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) = 0

goal (2 subgoals):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
 2. u \<in> {pz--z} \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infdist u (\<Union>x\<in>X. cball x r) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) = 0

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
using quasiconvexC[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) = 0
0 \<le> C

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C

goal (1 subgoal):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
u \<in> G

goal (1 subgoal):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
have "infdist u (\<Union>x\<in>X. cball x r) \<le> infdist u X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> infdist u X
[PROOF STEP]
apply (rule infdist_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. X \<subseteq> (\<Union>x\<in>X. cball x r)
 2. X \<noteq> {}
[PROOF STEP]
using assms(2) py(1)
[PROOF STATE]
proof (prove)
using this:
0 \<le> r
py \<in> X

goal (2 subgoals):
 1. X \<subseteq> (\<Union>x\<in>X. cball x r)
 2. X \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) \<le> infdist u X

goal (1 subgoal):
 1. u \<in> G \<Longrightarrow> infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infdist u (\<Union>x\<in>X. cball x r) \<le> infdist u X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) \<le> infdist u X

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
using 2 G(2)
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) \<le> infdist u X
u \<in> G
\<forall>p\<in>G. infdist p X \<le> C

goal (1 subgoal):
 1. infdist u (\<Union>x\<in>X. cball x r) \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
have "infdist w (\<Union>x\<in>X. cball x r) \<le> infdist u (\<Union>x\<in>X. cball x r) + dist w u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> infdist u (\<Union>x\<in>X. cball x r) + dist w u
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
infdist w (\<Union>x\<in>X. cball x r) \<le> infdist u (\<Union>x\<in>X. cball x r) + dist w u

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C
infdist w (\<Union>x\<in>X. cball x r) \<le> infdist u (\<Union>x\<in>X. cball x r) + dist w u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C
infdist w (\<Union>x\<in>X. cball x r) \<le> infdist u (\<Union>x\<in>X. cball x r) + dist w u

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
using A u(2)
[PROOF STATE]
proof (prove)
using this:
infdist u (\<Union>x\<in>X. cball x r) \<le> C
infdist w (\<Union>x\<in>X. cball x r) \<le> infdist u (\<Union>x\<in>X. cball x r) + dist w u
infdist w ({y--py} \<union> G \<union> {pz--z}) \<le> 8 * deltaG TYPE('a)
infdist w ({y--py} \<union> G \<union> {pz--z}) = dist w u

goal (1 subgoal):
 1. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?w \<in> {y--z} \<Longrightarrow> infdist ?w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> (\<Union>x\<in>X. cball x r); y \<in> (\<Union>x\<in>X. cball x r)\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> (\<forall>z\<in>G. infdist z (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
show "\<exists>G. geodesic_segment_between G y z \<and> (\<forall>w\<in>G. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>G. geodesic_segment_between G y z \<and> (\<forall>w\<in>G. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
apply (rule exI[of _ "{y--z}"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between {y--z} y z \<and> (\<forall>w\<in>{y--z}. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
?w \<in> {y--z} \<Longrightarrow> infdist ?w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a)

goal (1 subgoal):
 1. geodesic_segment_between {y--z} y z \<and> (\<forall>w\<in>{y--z}. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>G. geodesic_segment_between G y z \<and> (\<forall>w\<in>G. infdist w (\<Union>x\<in>X. cball x r) \<le> C + 8 * deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) dist_along_quasiconvex:
  assumes "quasiconvex C G" "p \<in> proj_set x G" "y \<in> G"
  shows "dist x p + dist p y \<le> dist x y + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have *: "p \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> G
[PROOF STEP]
using assms proj_setD
[PROOF STATE]
proof (prove)
using this:
quasiconvex C G
p \<in> proj_set x G
y \<in> G
?y \<in> proj_set ?x ?A \<Longrightarrow> ?y \<in> ?A
?y \<in> proj_set ?x ?A \<Longrightarrow> dist ?x ?y = infdist ?x ?A

goal (1 subgoal):
 1. p \<in> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> G

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
obtain H where H: "geodesic_segment_between H p y" "\<And>q. q \<in> H \<Longrightarrow> infdist q G \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>H. \<lbrakk>geodesic_segment_between H p y; \<And>q. q \<in> H \<Longrightarrow> infdist q G \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quasiconvexD[OF assms(1) * assms(3)]
[PROOF STATE]
proof (prove)
using this:
\<exists>Ga. geodesic_segment_between Ga p y \<and> (\<forall>z\<in>Ga. infdist z G \<le> C)

goal (1 subgoal):
 1. (\<And>H. \<lbrakk>geodesic_segment_between H p y; \<And>q. q \<in> H \<Longrightarrow> infdist q G \<le> C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between H p y
?q \<in> H \<Longrightarrow> infdist ?q G \<le> C

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have "\<exists>m\<in>H. infdist x H = dist x m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<in>H. infdist x H = dist x m
[PROOF STEP]
apply (rule infdist_proper_attained[of H x])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper H
 2. H \<noteq> {}
[PROOF STEP]
using geodesic_segment_topology[OF geodesic_segmentI[OF H(1)]]
[PROOF STATE]
proof (prove)
using this:
compact H
connected H
path_connected H
bounded H
closed H
H \<noteq> {}
proper H

goal (2 subgoals):
 1. proper H
 2. H \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<in>H. infdist x H = dist x m

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<in>H. infdist x H = dist x m
[PROOF STEP]
obtain m where m: "m \<in> H" "infdist x H = dist x m"
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<in>H. infdist x H = dist x m

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<in> H; infdist x H = dist x m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<in> H
infdist x H = dist x m

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> H
infdist x H = dist x m
[PROOF STEP]
have I: "dist x m \<le> Gromov_product_at x p y + 2 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
m \<in> H
infdist x H = dist x m

goal (1 subgoal):
 1. dist x m \<le> Gromov_product_at x p y + 2 * deltaG TYPE('a)
[PROOF STEP]
using infdist_triangle_side[OF H(1), of x]
[PROOF STATE]
proof (prove)
using this:
m \<in> H
infdist x H = dist x m
infdist x H \<le> Gromov_product_at x p y + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x m \<le> Gromov_product_at x p y + 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x m \<le> Gromov_product_at x p y + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have "dist x p - dist x m - C \<le> e" if "e > 0" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
have "\<exists>r\<in>G. dist m r < infdist m G + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>G. dist m r < infdist m G + e
[PROOF STEP]
apply (rule infdist_almost_attained)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. infdist m G < infdist m G + e
 2. G \<noteq> {}
[PROOF STEP]
using \<open>e > 0\<close> assms(3)
[PROOF STATE]
proof (prove)
using this:
0 < e
y \<in> G

goal (2 subgoals):
 1. infdist m G < infdist m G + e
 2. G \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>G. dist m r < infdist m G + e

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r\<in>G. dist m r < infdist m G + e
[PROOF STEP]
obtain r where r: "r \<in> G" "dist m r < infdist m G + e"
[PROOF STATE]
proof (prove)
using this:
\<exists>r\<in>G. dist m r < infdist m G + e

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> G; dist m r < infdist m G + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> G
dist m r < infdist m G + e

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> G
dist m r < infdist m G + e
[PROOF STEP]
have *: "dist m r \<le> C + e"
[PROOF STATE]
proof (prove)
using this:
r \<in> G
dist m r < infdist m G + e

goal (1 subgoal):
 1. dist m r \<le> C + e
[PROOF STEP]
using H(2)[OF \<open>m \<in> H\<close>]
[PROOF STATE]
proof (prove)
using this:
r \<in> G
dist m r < infdist m G + e
infdist m G \<le> C

goal (1 subgoal):
 1. dist m r \<le> C + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist m r \<le> C + e

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
have "dist x p \<le> dist x r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x p \<le> dist x r
[PROOF STEP]
using \<open>r \<in> G\<close> assms(2) proj_set_dist_le
[PROOF STATE]
proof (prove)
using this:
r \<in> G
p \<in> proj_set x G
\<lbrakk>?y \<in> ?A; ?p \<in> proj_set ?x ?A\<rbrakk> \<Longrightarrow> dist ?x ?p \<le> dist ?x ?y

goal (1 subgoal):
 1. dist x p \<le> dist x r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist x p \<le> dist x r

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x p \<le> dist x r

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
have "... \<le> dist x m + dist m r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x r \<le> dist x m + dist m r
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist x r \<le> dist x m + dist m r

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x p \<le> dist x m + dist m r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x p \<le> dist x m + dist m r

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist x p \<le> dist x m + dist m r
dist m r \<le> C + e

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> e
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist x p - dist x m - C \<le> e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> dist x p - dist x m - C \<le> ?e

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?e \<Longrightarrow> dist x p - dist x m - C \<le> ?e
[PROOF STEP]
have "dist x p - dist x m - C \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> dist x p - dist x m - C \<le> ?e

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> 0
[PROOF STEP]
using dense_ge
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> dist x p - dist x m - C \<le> ?e
(\<And>x. ?z < x \<Longrightarrow> ?y \<le> x) \<Longrightarrow> ?y \<le> ?z

goal (1 subgoal):
 1. dist x p - dist x m - C \<le> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist x p - dist x m - C \<le> 0

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x p - dist x m - C \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x p - dist x m - C \<le> 0

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
dist x p - dist x m - C \<le> 0
dist x m \<le> Gromov_product_at x p y + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
unfolding Gromov_product_at_def
[PROOF STATE]
proof (prove)
using this:
dist x p - dist x m - C \<le> 0
dist x m \<le> (dist x p + dist x y - dist p y) / 2 + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) proj_along_quasiconvex_contraction:
  assumes "quasiconvex C G" "px \<in> proj_set x G" "py \<in> proj_set y G"
  shows "dist px py \<le> max (5 * deltaG(TYPE('a)) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG(TYPE('a)) + 4 * C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
have "px \<in> G" "py \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. px \<in> G &&& py \<in> G
[PROOF STEP]
using assms proj_setD
[PROOF STATE]
proof (prove)
using this:
quasiconvex C G
px \<in> proj_set x G
py \<in> proj_set y G
?y \<in> proj_set ?x ?A \<Longrightarrow> ?y \<in> ?A
?y \<in> proj_set ?x ?A \<Longrightarrow> dist ?x ?y = infdist ?x ?A

goal (1 subgoal):
 1. px \<in> G &&& py \<in> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
px \<in> G
py \<in> G

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
have "(dist x px + dist px py - 4 * deltaG(TYPE('a)) - 2 * C) + (dist y py + dist py px - 4 *deltaG(TYPE('a)) - 2 * C)
        \<le> dist x py + dist y px"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C + (dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C) \<le> dist x py + dist y px
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C \<le> dist x py
 2. dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C \<le> dist y px
[PROOF STEP]
using dist_along_quasiconvex[OF assms(1) assms(2) \<open>py \<in> G\<close>] dist_along_quasiconvex[OF assms(1) assms(3) \<open>px \<in> G\<close>]
[PROOF STATE]
proof (prove)
using this:
dist x px + dist px py \<le> dist x py + 4 * deltaG TYPE('a) + 2 * C
dist y py + dist py px \<le> dist y px + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C \<le> dist x py
 2. dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C \<le> dist y px
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C + (dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C) \<le> dist x py + dist y px

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C + (dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C) \<le> dist x py + dist y px

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
have "... \<le> max (dist x y + dist py px) (dist x px + dist py y) + 2 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x py + dist y px \<le> max (dist x y + dist py px) (dist x px + dist py y) + 2 * deltaG TYPE('a)
[PROOF STEP]
by (rule hyperb_quad_ineq)
[PROOF STATE]
proof (state)
this:
dist x py + dist y px \<le> max (dist x y + dist py px) (dist x px + dist py y) + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C + (dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C) \<le> max (dist x y + dist py px) (dist x px + dist py y) + 2 * deltaG TYPE('a)
[PROOF STEP]
have *: "dist x px + dist y py + 2 * dist px py
          \<le> max (dist x y + dist py px) (dist x px + dist py y) + 10 * deltaG(TYPE('a)) + 4 * C"
[PROOF STATE]
proof (prove)
using this:
dist x px + dist px py - 4 * deltaG TYPE('a) - 2 * C + (dist y py + dist py px - 4 * deltaG TYPE('a) - 2 * C) \<le> max (dist x y + dist py px) (dist x px + dist py y) + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x px + dist y py + 2 * dist px py \<le> max (dist x y + dist py px) (dist x px + dist py y) + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist x px + dist y py + 2 * dist px py \<le> max (dist x y + dist py px) (dist x px + dist py y) + 10 * deltaG TYPE('a) + 4 * C

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
proof (cases "dist x y + dist py px \<ge> dist x px + dist py y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
 2. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dist x px + dist py y \<le> dist x y + dist py px

goal (2 subgoals):
 1. dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
 2. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x px + dist py y \<le> dist x y + dist py px
[PROOF STEP]
have "dist x px + dist y py + 2 * dist px py \<le> dist x y + dist py px + 10 * deltaG(TYPE('a)) + 4 * C"
[PROOF STATE]
proof (prove)
using this:
dist x px + dist py y \<le> dist x y + dist py px

goal (1 subgoal):
 1. dist x px + dist y py + 2 * dist px py \<le> dist x y + dist py px + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
dist x px + dist py y \<le> dist x y + dist py px
dist x px + dist y py + 2 * dist px py \<le> max (dist x y + dist py px) (dist x px + dist py y) + 10 * deltaG TYPE('a) + 4 * C

goal (1 subgoal):
 1. dist x px + dist y py + 2 * dist px py \<le> dist x y + dist py px + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x px + dist y py + 2 * dist px py \<le> dist x y + dist py px + 10 * deltaG TYPE('a) + 4 * C

goal (2 subgoals):
 1. dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
 2. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x px + dist y py + 2 * dist px py \<le> dist x y + dist py px + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x px + dist y py + 2 * dist px py \<le> dist x y + dist py px + 10 * deltaG TYPE('a) + 4 * C

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)

goal (1 subgoal):
 1. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> dist x px + dist py y \<le> dist x y + dist py px

goal (1 subgoal):
 1. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> dist x px + dist py y \<le> dist x y + dist py px
[PROOF STEP]
have "dist x px + dist y py + 2 * dist px py \<le> dist x px + dist py y + 10 * deltaG(TYPE('a)) + 4 * C"
[PROOF STATE]
proof (prove)
using this:
\<not> dist x px + dist py y \<le> dist x y + dist py px

goal (1 subgoal):
 1. dist x px + dist y py + 2 * dist px py \<le> dist x px + dist py y + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<not> dist x px + dist py y \<le> dist x y + dist py px
dist x px + dist y py + 2 * dist px py \<le> max (dist x y + dist py px) (dist x px + dist py y) + 10 * deltaG TYPE('a) + 4 * C

goal (1 subgoal):
 1. dist x px + dist y py + 2 * dist px py \<le> dist x px + dist py y + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x px + dist y py + 2 * dist px py \<le> dist x px + dist py y + 10 * deltaG TYPE('a) + 4 * C

goal (1 subgoal):
 1. \<not> dist x px + dist py y \<le> dist x y + dist py px \<Longrightarrow> dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x px + dist y py + 2 * dist px py \<le> dist x px + dist py y + 10 * deltaG TYPE('a) + 4 * C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x px + dist y py + 2 * dist px py \<le> dist x px + dist py y + 10 * deltaG TYPE('a) + 4 * C

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist px py \<le> max (5 * deltaG TYPE('a) + 2 * C) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) proj_along_quasiconvex_contraction':
  assumes "quasiconvex C G" "px \<in> proj_set x G" "py \<in> proj_set y G"
  shows "dist px py \<le> dist x y + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
proof (cases "dist y py \<le> dist x px")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
 2. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dist y py \<le> dist x px

goal (2 subgoals):
 1. dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
 2. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have "dist x px + dist px py \<le> dist x py + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x px + dist px py \<le> dist x py + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by (rule dist_along_quasiconvex[OF assms(1) assms(2) proj_setD(1)[OF assms(3)]])
[PROOF STATE]
proof (state)
this:
dist x px + dist px py \<le> dist x py + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
 2. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x px + dist px py \<le> dist x py + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
 2. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have "... \<le> (dist x y + dist y py) + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x py + 4 * deltaG TYPE('a) + 2 * C \<le> dist x y + dist y py + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist x py + 4 * deltaG TYPE('a) + 2 * C \<le> dist x y + dist y py + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
 2. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x px + dist px py \<le> dist x y + dist y py + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x px + dist px py \<le> dist x y + dist y py + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
dist x px + dist px py \<le> dist x y + dist y py + 4 * deltaG TYPE('a) + 2 * C
dist y py \<le> dist x px

goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> dist y py \<le> dist x px

goal (1 subgoal):
 1. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have "dist y py + dist py px \<le> dist y px + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist y py + dist py px \<le> dist y px + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by (rule dist_along_quasiconvex[OF assms(1) assms(3) proj_setD(1)[OF assms(2)]])
[PROOF STATE]
proof (state)
this:
dist y py + dist py px \<le> dist y px + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist y py + dist py px \<le> dist y px + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have "... \<le> (dist y x + dist x px) + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist y px + 4 * deltaG TYPE('a) + 2 * C \<le> dist y x + dist x px + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist y px + 4 * deltaG TYPE('a) + 2 * C \<le> dist y x + dist x px + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. \<not> dist y py \<le> dist x px \<Longrightarrow> dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist y py + dist py px \<le> dist y x + dist x px + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist y py + dist py px \<le> dist y x + dist x px + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
dist y py + dist py px \<le> dist y x + dist x px + 4 * deltaG TYPE('a) + 2 * C
\<not> dist y py \<le> dist x px

goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) dist_along_geodesic:
  assumes "geodesic_segment G" "p \<in> proj_set x G" "y \<in> G"
  shows "dist x p + dist p y \<le> dist x y + 4 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a)
[PROOF STEP]
using dist_along_quasiconvex[OF quasiconvex_of_geodesic[OF assms(1)] assms(2) assms(3)]
[PROOF STATE]
proof (prove)
using this:
dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a) + 2 * 0

goal (1 subgoal):
 1. dist x p + dist p y \<le> dist x y + 4 * deltaG TYPE('a)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) proj_along_geodesic_contraction:
  assumes "geodesic_segment G" "px \<in> proj_set x G" "py \<in> proj_set y G"
  shows "dist px py \<le> max (5 * deltaG(TYPE('a))) (dist x y - dist px x - dist py y + 10 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a))
[PROOF STEP]
using proj_along_quasiconvex_contraction[OF quasiconvex_of_geodesic[OF assms(1)] assms(2) assms(3)]
[PROOF STATE]
proof (prove)
using this:
dist px py \<le> max (5 * deltaG TYPE('a) + 2 * 0) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) + 4 * 0)

goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a))
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) proj_along_geodesic_contraction':
  assumes "geodesic_segment G" "px \<in> proj_set x G" "py \<in> proj_set y G"
  shows "dist px py \<le> dist x y + 4 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a)
[PROOF STEP]
using proj_along_quasiconvex_contraction'[OF quasiconvex_of_geodesic[OF assms(1)] assms(2) assms(3)]
[PROOF STATE]
proof (prove)
using this:
dist px py \<le> dist x y + 4 * deltaG TYPE('a) + 2 * 0

goal (1 subgoal):
 1. dist px py \<le> dist x y + 4 * deltaG TYPE('a)
[PROOF STEP]
by auto