[STATEMENT]
lemma GF_advice_sync_less:
  assumes "\<And>i. i < n \<Longrightarrow> \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n af \<phi> (w [i \<rightarrow> j + i])[X]\<^sub>\<nu>"
  assumes "\<exists>j. suffix (n + j) w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> j + n])[X]\<^sub>\<nu>"
  shows "\<exists>k \<ge> n. (\<forall>j < n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
let ?index = "\<lambda>i. min i n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
let ?formula = "\<lambda>i. if (i < n) then \<phi> else \<psi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
assume "i < Suc n"
[PROOF STATE]
proof (state)
this:
i < Suc n

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < Suc n
[PROOF STEP]
have min_def: "min i n = i"
[PROOF STATE]
proof (prove)
using this:
i < Suc n

goal (1 subgoal):
 1. min i n = i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
min i n = i

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "\<exists>j. suffix ((?index i) + j) w \<Turnstile>\<^sub>n af (?formula i) (w [?index i \<rightarrow> (?index i) + j])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. suffix (min i n + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> min i n + j])[X]\<^sub>\<nu>
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. suffix (i + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [i \<rightarrow> i + j])[X]\<^sub>\<nu>
[PROOF STEP]
by (cases "i < n")
         (metis (full_types) assms(1) add.commute, metis (full_types) assms(2) \<open>i < Suc n\<close> add.commute  less_SucE)
[PROOF STATE]
proof (state)
this:
\<exists>j. suffix (min i n + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> min i n + j])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>
[PROOF STEP]
obtain k where leq: "(\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k)"
    and suffix: "\<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
using this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k; \<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GF_advice_sync[of "Suc n" ?index w ?formula X]
[PROOF STATE]
proof (prove)
using this:
?i2 < Suc n \<Longrightarrow> \<exists>j. suffix (min ?i2 n + j) w \<Turnstile>\<^sub>n af (if ?i2 < n then \<phi> else \<psi>) (w [min ?i2 n \<rightarrow> min ?i2 n + j])[X]\<^sub>\<nu>
(\<And>i. i < Suc n \<Longrightarrow> \<exists>j. suffix (min i n + j) w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> min i n + j])[X]\<^sub>\<nu>) \<Longrightarrow> \<exists>k. \<forall>i<Suc n. min i n \<le> k \<and> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>\<And>i. i < Suc n \<Longrightarrow> min i n \<le> k; \<And>i. i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if i < n then \<phi> else \<psi>) (w [min i n \<rightarrow> k])[X]\<^sub>\<nu>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?i < Suc n \<Longrightarrow> min ?i n \<le> k
?i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if ?i < n then \<phi> else \<psi>) (w [min ?i n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "\<forall>j < n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
using suffix
[PROOF STATE]
proof (prove)
using this:
?i < Suc n \<Longrightarrow> suffix k w \<Turnstile>\<^sub>n af (if ?i < n then \<phi> else \<psi>) (w [min ?i n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
by (metis (full_types) less_SucI min.strict_order_iff)
[PROOF STATE]
proof (state)
this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
using suffix[of n, simplified]
[PROOF STATE]
proof (prove)
using this:
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
have "k \<ge> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
using leq
[PROOF STATE]
proof (prove)
using this:
?i < Suc n \<Longrightarrow> min ?i n \<le> k

goal (1 subgoal):
 1. n \<le> k
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
n \<le> k

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
n \<le> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>
suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
n \<le> k

goal (1 subgoal):
 1. \<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k\<ge>n. (\<forall>j<n. suffix k w \<Turnstile>\<^sub>n af \<phi> (w [j \<rightarrow> k])[X]\<^sub>\<nu>) \<and> suffix k w \<Turnstile>\<^sub>n af \<psi> (w [n \<rightarrow> k])[X]\<^sub>\<nu>

goal:
No subgoals!
[PROOF STEP]
qed