# Theory Transition_Functions

```(*
Author:   Benedikt Seidl
*)

section ‹Transition Functions for Deterministic Automata›

theory Transition_Functions
imports
"../Logical_Characterization/After"
begin

text ‹
This theory defines three functions based on the ``after''-function
which we use as transition functions for deterministic automata.
›

locale transition_functions =
begin

subsection ‹After Functions with Resets for @{term "GF(μLTL)"} and @{term "FG(νLTL)"}›

definition af_letter⇩F :: "'a ltln ⇒ 'a ltln ⇒ 'a set ⇒ 'a ltln"
where
"af_letter⇩F φ ψ ν = (if ψ ∼ true⇩n then F⇩n φ else af_letter ψ ν)"

definition af_letter⇩G :: "'a ltln ⇒ 'a ltln ⇒ 'a set ⇒ 'a ltln"
where
"af_letter⇩G φ ψ ν = (if ψ ∼ false⇩n then G⇩n φ else af_letter ψ ν)"

abbreviation af⇩F :: "'a ltln ⇒ 'a ltln ⇒ 'a set list ⇒ 'a ltln"
where
"af⇩F φ ψ w ≡ foldl (af_letter⇩F φ) ψ w"

abbreviation af⇩G :: "'a ltln ⇒ 'a ltln ⇒ 'a set list ⇒ 'a ltln"
where
"af⇩G φ ψ w ≡ foldl (af_letter⇩G φ) ψ w"

lemma af⇩F_step:
"af⇩F φ ψ w ∼ true⇩n ⟹ af⇩F φ ψ (w @ [ν]) = F⇩n φ"
by (induction w rule: rev_induct) (auto simp: af_letter⇩F_def)

lemma af⇩G_step:
"af⇩G φ ψ w ∼ false⇩n ⟹ af⇩G φ ψ (w @ [ν]) = G⇩n φ"
by (induction w rule: rev_induct) (auto simp: af_letter⇩G_def)

lemma af⇩F_segments:
"af⇩F φ ψ w = F⇩n φ ⟹ af⇩F φ ψ (w @ w') = af⇩F φ (F⇩n φ) w'"
by simp

lemma af⇩G_segments:
"af⇩G φ ψ w = G⇩n φ ⟹ af⇩G φ ψ (w @ w') = af⇩G φ (G⇩n φ) w'"
by simp

lemma af_not_true_implies_af_equals_af⇩F:
"(⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ true⇩n) ⟹ af⇩F φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
case (snoc x xs)

then have "af⇩F φ ψ xs = af ψ xs"
by simp

moreover

have "¬ af ψ xs ∼ true⇩n"
using snoc.prems by blast

ultimately show ?case
by (metis af_letter⇩F_def foldl_Cons foldl_Nil foldl_append)
qed simp

lemma af_not_false_implies_af_equals_af⇩G:
"(⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ false⇩n) ⟹ af⇩G φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
case (snoc x xs)

then have "af⇩G φ ψ xs = af ψ xs"
by simp

moreover

have "¬ af ψ xs ∼ false⇩n"
using snoc.prems by blast

ultimately show ?case
by (metis af_letter⇩G_def foldl_Cons foldl_Nil foldl_append)
qed simp

lemma af⇩F_not_true_implies_af_equals_af⇩F:
"(⋀xs ys. w = xs @ ys ⟹ ¬ af⇩F φ ψ xs ∼ true⇩n) ⟹ af⇩F φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
case (snoc x xs)

then have "af⇩F φ ψ xs = af ψ xs"
by simp

moreover

have "¬ af⇩F φ ψ xs ∼ true⇩n"
using snoc.prems by blast

ultimately show ?case
by (metis af_letter⇩F_def foldl_Cons foldl_Nil foldl_append)
qed simp

lemma af⇩G_not_false_implies_af_equals_af⇩G:
"(⋀xs ys. w = xs @ ys ⟹ ¬ af⇩G φ ψ xs ∼ false⇩n) ⟹ af⇩G φ ψ w = af ψ w"
proof (induction w rule: rev_induct)
case (snoc x xs)

then have "af⇩G φ ψ xs = af ψ xs"
by simp

moreover

have "¬ af⇩G φ ψ xs ∼ false⇩n"
using snoc.prems by blast

ultimately show ?case
by (metis af_letter⇩G_def foldl_Cons foldl_Nil foldl_append)
qed simp

lemma af⇩F_true_implies_af_true:
"af⇩F φ ψ w ∼ true⇩n ⟹ af ψ w ∼ true⇩n"
by (metis af_append_true af_not_true_implies_af_equals_af⇩F)

lemma af⇩G_false_implies_af_false:
"af⇩G φ ψ w ∼ false⇩n ⟹ af ψ w ∼ false⇩n"
by (metis af_append_false af_not_false_implies_af_equals_af⇩G)

lemma af_equiv_true_af⇩F_prefix_true:
"af ψ w ∼ true⇩n ⟹ ∃xs ys. w = xs @ ys ∧ af⇩F φ ψ xs ∼ true⇩n"
proof (induction w rule: rev_induct)
case (snoc a w)
then show ?case
proof (cases "af ψ w ∼ true⇩n")
case False

then have "⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ true⇩n"
using af_append_true by blast

then have "af⇩F φ ψ w = af ψ w"
using af_not_true_implies_af_equals_af⇩F by auto

then have "af⇩F φ ψ (w @ [a]) = af ψ (w @ [a])"

then show ?thesis
by (metis append_Nil2 snoc.prems)
qed (insert snoc, force)

lemma af_equiv_false_af⇩G_prefix_false:
"af ψ w ∼ false⇩n ⟹ ∃xs ys. w = xs @ ys ∧ af⇩G φ ψ xs ∼ false⇩n"
proof (induction w rule: rev_induct)
case (snoc a w)
then show ?case
proof (cases "af ψ w ∼ false⇩n")
case False

then have "⋀xs ys. w = xs @ ys ⟹ ¬ af ψ xs ∼ false⇩n"
using af_append_false by blast

then have "af⇩G φ ψ w = af ψ w"
using af_not_false_implies_af_equals_af⇩G by auto

then have "af⇩G φ ψ (w @ [a]) = af ψ (w @ [a])"

then show ?thesis
by (metis append_Nil2 snoc.prems)
qed (insert snoc, force)

lemma append_take_drop:
"w = xs @ ys ⟷ xs = take (length xs) w ∧ ys = drop (length xs) w"
by (metis append_eq_conv_conj)

lemma subsequence_split:
"(w [i → j]) = xs @ ys ⟹ xs = (w [i → i + length xs])"

lemma subsequence_append_general:
"i ≤ k ⟹ k ≤ j ⟹ (w [i → j]) = (w [i → k]) @ (w [k → j])"
by (metis le_Suc_ex map_append subsequence_def upt_add_eq_append)

lemma af⇩F_semantics_rtl:
assumes
"∀i. ∃j>i. af⇩F φ (F⇩n φ) (w [0 → j]) ∼ true⇩n"
shows
"∀i. ∃j. af (F⇩n φ) (w [i → j]) ∼⇩L true⇩n"
proof
fix i
from assms obtain j where "j > i" and "af⇩F φ (F⇩n φ) (w [0 → j]) ∼ true⇩n"
by blast
then have X: "af⇩F φ (F⇩n φ) (w [0 → Suc j]) = F⇩n φ"
using af⇩F_step by auto

obtain k where "k > j" and "af⇩F φ (F⇩n φ) (w [0 → k]) ∼ true⇩n"
using assms using Suc_le_eq by blast
then have "af⇩F φ (F⇩n φ) (w [Suc j → k]) ∼ true⇩n"
using af⇩F_segments[OF X] by (metis le_Suc_ex le_simps(3) subsequence_append)
then have "af (F⇩n φ) (w [Suc j → k]) ∼ true⇩n"
using af⇩F_true_implies_af_true by blast
then show "∃k. af (F⇩n φ) (w [i → k]) ∼⇩L true⇩n"
by (metis (full_types) af_F_prefix_lang_equiv_true eq_implies_lang subsequence_append_general Suc_le_eq ‹i < j› ‹j < k› less_SucI order.order_iff_strict)
qed

lemma af⇩F_semantics_ltr:
assumes
"∀i. ∃j. af (F⇩n φ) (w [i → j]) ∼ true⇩n"
shows
"∀i. ∃j>i. af⇩F φ (F⇩n φ) (w [0 → j]) ∼ true⇩n"
proof (rule ccontr)
define resets where "resets = {i. af⇩F φ (F⇩n φ) (w [0 → i]) ∼ true⇩n}"
define m where "m = (if resets = {} then 0 else Suc (Max resets))"

assume "¬ (∀i. ∃j>i. af⇩F φ (F⇩n φ) (w [0 → j]) ∼ true⇩n)"

then have "finite resets"
using infinite_nat_iff_unbounded resets_def by force
then have "resets ≠ {} ⟹ af⇩F φ (F⇩n φ) (w [0 → Max resets]) ∼ true⇩n"
unfolding resets_def using Max_in by blast
then have m_reset: "af⇩F φ (F⇩n φ) (w [0 → m]) = F⇩n φ"
unfolding m_def using af⇩F_step by auto

{
fix i
assume "i ≥ m"

with m_reset have "¬ af⇩F φ (F⇩n φ) (w [0 → i]) ∼ true⇩n"
by (metis (mono_tags, lifting) Max_ge_iff Suc_n_not_le_n ‹finite resets› empty_Collect_eq m_def mem_Collect_eq resets_def)
with m_reset have "¬ af⇩F φ  (F⇩n φ)(w [m → i]) ∼ true⇩n"
by (metis (mono_tags, opaque_lifting) ‹m ≤ i› af⇩F_segments bot_nat_def le0 subsequence_append_general)
}

then have "∄j. af⇩F φ (F⇩n φ) (w [m → j]) ∼ true⇩n"
by (metis le_cases subseq_to_smaller)
then have "∄j. af (F⇩n φ) (w [m → j]) ∼ true⇩n"
by (metis af_equiv_true_af⇩F_prefix_true subsequence_split)
then show False
using assms by blast
qed

lemma af⇩G_semantics_rtl:
assumes
"∃i. ∀j>i. ¬ af⇩G φ (G⇩n φ) (w [0 → j]) ∼ false⇩n"
shows
"∃i. ∀j. ¬ af (G⇩n φ) (w [i → j]) ∼ false⇩n"
proof
define resets where "resets = {i. af⇩G φ (G⇩n φ) (w [0 → i]) ∼ false⇩n}"
define m where "m = (if resets = {} then 0 else Suc (Max resets))"

from assms have "finite resets"
by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)
then have "resets ≠ {} ⟹ af⇩G φ (G⇩n φ) (w [0 → Max resets]) ∼ false⇩n"
unfolding resets_def using Max_in by blast
then have m_reset: "af⇩G φ (G⇩n φ) (w [0 → m]) = G⇩n φ"
unfolding m_def using af⇩G_step by auto

{
fix i
assume "i ≥ m"

with m_reset have "¬ af⇩G φ (G⇩n φ) (w [0 → i]) ∼ false⇩n"
by (metis (mono_tags, lifting) Max_ge_iff Suc_n_not_le_n ‹finite resets› empty_Collect_eq m_def mem_Collect_eq resets_def)
with m_reset have "¬ af⇩G φ (G⇩n φ) (w [m → i]) ∼ false⇩n"
by (metis (mono_tags, opaque_lifting) ‹m ≤ i› af⇩G_segments bot_nat_def le0 subsequence_append_general)
}

then have "∀j. ¬ af⇩G φ (G⇩n φ) (w [m → j]) ∼ false⇩n"
by (metis le_cases subseq_to_smaller)
then show "∀j. ¬ af (G⇩n φ) (w [m → j]) ∼ false⇩n"
by (metis af_equiv_false_af⇩G_prefix_false subsequence_split)
qed

lemma af⇩G_semantics_ltr:
assumes
"∃i. ∀j. ¬ af (G⇩n φ) (w [i → j]) ∼⇩L false⇩n"
shows
"∃i. ∀j>i. ¬ af⇩G φ (G⇩n φ) (w [0 → j]) ∼ false⇩n"
proof (rule ccontr, auto)
assume 1: "∀i. ∃j>i. af⇩G φ (G⇩n φ) (w [0 → j]) ∼ false⇩n"

{
fix i
obtain j where "j > i" and "af⇩G φ (G⇩n φ) (w [0 → j]) ∼ false⇩n"
using 1 by blast
then have X: "af⇩G φ (G⇩n φ) (w [0 → Suc j]) = G⇩n φ"
using af⇩G_step by auto

obtain k where "k > j" and "af⇩G φ (G⇩n φ) (w [0 → k]) ∼ false⇩n"
using 1 using Suc_le_eq by blast
then have "af⇩G φ (G⇩n φ) (w [Suc j → k]) ∼ false⇩n"
using af⇩G_segments[OF X] by (metis le_Suc_ex le_simps(3) subsequence_append)
then have "af (G⇩n φ) (w [Suc j → k]) ∼ false⇩n"
using af⇩G_false_implies_af_false by fastforce
then have "af (G⇩n φ) (w [Suc j → k]) ∼⇩L false⇩n"
using eq_implies_lang by fastforce
then have "af (G⇩n φ) (w [i → k]) ∼⇩L false⇩n"
by (metis (full_types) af_G_prefix_lang_equiv_false subsequence_append_general Suc_le_eq ‹i < j› ‹j < k› less_SucI order.order_iff_strict)
then have "∃j. af (G⇩n φ) (w [i → j]) ∼⇩L false⇩n"
by fast
}

then show False
using assms by blast
qed

definition af_letter⇩ν :: "'a ltln set ⇒ 'a ltln × 'a ltln ⇒ 'a set ⇒ 'a ltln × 'a ltln"
where
"af_letter⇩ν X p ν = (if snd p ∼ false⇩n
then (af_letter (fst p) ν, (normalise (af_letter (fst p) ν))[X]⇩ν)
else (af_letter (fst p) ν, af_letter (snd p) ν))"

abbreviation af⇩ν :: "'a ltln set ⇒ 'a ltln × 'a ltln ⇒ 'a set list ⇒ 'a ltln × 'a ltln"
where
"af⇩ν X p w ≡ foldl (af_letter⇩ν X) p w"

lemma af_letter⇩ν_fst[simp]:
"fst (af_letter⇩ν X p ν) = af_letter (fst p) ν"

lemma af_letter⇩ν_snd[simp]:
"snd p ∼ false⇩n ⟹ snd (af_letter⇩ν X p ν) = (normalise (af_letter (fst p) ν))[X]⇩ν"
"¬ (snd p) ∼ false⇩n ⟹ snd (af_letter⇩ν X p ν) = af_letter (snd p) ν"

lemma af⇩ν_fst:
"fst (af⇩ν X p w) = af (fst p) w"
by (induction w rule: rev_induct) simp+

lemma af⇩ν_snd:
"¬ af (snd p) w ∼ false⇩n ⟹ snd (af⇩ν X p w) = af (snd p) w"
by (induction w rule: rev_induct) (simp_all, metis af_letter⇩ν_snd(2) af_letter.simps(2) af_letter_congruent)

lemma af⇩ν_snd':
"∀i. ¬ snd (af⇩ν X p (take i w)) ∼ false⇩n ⟹ snd (af⇩ν X p w) = af (snd p) w"
by (induction w rule: rev_induct) (simp_all, metis af_letter⇩ν_snd(2) diff_is_0_eq foldl_Nil le_cases take_all take_eq_Nil)

lemma af⇩ν_step:
"snd (af⇩ν X (ξ, ζ) w) ∼ false⇩n ⟹ snd (af⇩ν X (ξ, ζ) (w @ [ν])) = (normalise (af ξ (w @ [ν])))[X]⇩ν"

lemma af⇩ν_segments:
"af⇩ν X (ξ, ζ) w = (af ξ w, (af ξ w)[X]⇩ν) ⟹ af⇩ν X (ξ, ζ) (w @ w') = af⇩ν X (af ξ w, (af ξ w)[X]⇩ν) w'"
by (induction w' rule: rev_induct) fastforce+

lemma af⇩ν_semantics_ltr:
assumes
"∃i. suffix i w ⊨⇩n (af φ (prefix i w))[X]⇩ν"
shows
"∃m. ∀k≥m. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc k) w)) ∼ false⇩n"
proof
define resets where "resets = {i. snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix i w)) ∼ false⇩n}"
define m where "m = (if resets = {} then 0 else Suc (Max resets))"

from assms obtain i where 1: "suffix i w ⊨⇩n (af φ (prefix i w))[X]⇩ν"
by blast

{
fix j
assume "i ≤ j" and "j ∈ resets"

let ?φ = "af φ (prefix (Suc j) w)"

from 1 have "∀n. suffix n (suffix i w) ⊨⇩n (normalise (af φ (prefix i w @ prefix n (suffix i w))))[X]⇩ν"

then have "suffix (Suc j) w ⊨⇩n (normalise (af φ (prefix (Suc j) w)))[X]⇩ν"
by (metis (no_types) ‹i ≤ j› add.right_neutral le_SucI le_Suc_ex subsequence_append subsequence_shift suffix_suffix)

then have "∀k>j. ¬ af ((normalise (af φ (prefix (Suc j) w)))[X]⇩ν) (w [Suc j → k]) ∼ false⇩n"
by (metis ltl_implies_satisfiable_prefix subsequence_prefix_suffix)

then have "∀k>j. ¬ snd (af⇩ν X (?φ, (normalise ?φ)[X]⇩ν) (w [Suc j → k])) ∼ false⇩n"
by (metis af⇩ν_snd snd_eqD)

moreover

{
have "fst (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc j) w)) = ?φ"

moreover

have "snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix j w)) ∼ false⇩n"
using ‹j ∈ resets› resets_def by blast

ultimately have "af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc j) w) = (?φ, (normalise ?φ)[X]⇩ν)"
by (metis (no_types) af⇩ν_step prod.collapse subseq_to_Suc zero_le)
}

ultimately have "∀k>j. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) ((w [0 → Suc j]) @ (w [Suc j → k]))) ∼ false⇩n"

then have "∀k>j. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix k w)) ∼ false⇩n"
by (metis Suc_leI le0 subsequence_append_general)

then have "∀k ∈ resets. k ≤ j"
using ‹j ∈ resets› resets_def le_less_linear by blast
}

then have "finite resets"
by (meson finite_nat_set_iff_bounded_le infinite_nat_iff_unbounded_le)

then have "resets ≠ {} ⟹ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Max resets) w)) ∼ false⇩n"
using Max_in resets_def by blast

then have "∀k≥m. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix k w)) ∼ false⇩n"
by (metis (mono_tags, lifting) Max_ge Suc_n_not_le_n ‹finite resets› empty_Collect_eq m_def mem_Collect_eq order.trans resets_def)

then show "∀k≥m. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc k) w)) ∼ false⇩n"
using le_SucI by blast
qed

lemma af⇩ν_semantics_rtl:
assumes
"∃n. ∀k≥n. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc k) w)) ∼ false⇩n"
shows
"∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν"
proof -
define resets where "resets = {i. snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix i w)) ∼ false⇩n}"
define m where "m = (if resets = {} then 0 else Suc (Max resets))"

from assms obtain n where "∀k≥n. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc k) w)) ∼ false⇩n"
by blast

then have "∀k>n. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix k w)) ∼ false⇩n"
by (metis le_SucE lessE less_imp_le_nat)

then have "finite resets"
by (metis (mono_tags, lifting) infinite_nat_iff_unbounded mem_Collect_eq resets_def)

then have "∀i≥m. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix i w)) ∼ false⇩n"
unfolding resets_def m_def using Max_ge not_less_eq_eq by auto

then have "∀i. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) ((w [0 → m]) @ (w [m → i]))) ∼ false⇩n"
by (metis le0 nat_le_linear subseq_to_smaller subsequence_append_general)

moreover

let ?φ = "af φ (prefix m w)"

have "resets ≠ {} ⟹ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Max resets) w)) ∼ false⇩n"
using Max_in ‹finite resets› resets_def by blast

then have prefix_φ': "snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix m w)) = (normalise ?φ)[X]⇩ν"
by (auto simp: GF_advice_congruent m_def af⇩ν_fst)

ultimately have "∀i. ¬ snd (af⇩ν X (?φ, (normalise ?φ)[X]⇩ν) (w [m → i])) ∼ false⇩n"
by (metis af⇩ν_fst foldl_append fst_conv prod.collapse)

then have "∀i. ¬ af ((normalise ?φ)[X]⇩ν) (w [m → i]) ∼ false⇩n"
by (metis prefix_φ' af⇩ν_fst af⇩ν_snd' fst_conv prod.collapse subsequence_take)

then have "suffix m w ⊨⇩n (normalise (af φ (prefix m w)))[X]⇩ν"

from this[THEN normalise_eventually_equivalent]
show "∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν"
qed

end

subsection ‹Reachability Bounds›

text ‹
We show that the reach of each after-function is bounded by the atomic
propositions of the input formula.
›

locale transition_functions_size = transition_functions +
assumes
normalise_nested_propos: "nested_prop_atoms φ ⊇ nested_prop_atoms (normalise φ)"
begin

lemma af_letter⇩F_nested_prop_atoms:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ) ⟹ nested_prop_atoms (af_letter⇩F φ ψ ν) ⊆ nested_prop_atoms (F⇩n φ)"
by (induction ψ) (auto simp: af_letter⇩F_def, insert af_letter_nested_prop_atoms, blast+)

lemma af⇩F_nested_prop_atoms:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ) ⟹ nested_prop_atoms (af⇩F φ ψ w) ⊆ nested_prop_atoms (F⇩n φ)"
by (induction w rule: rev_induct) (insert af_letter⇩F_nested_prop_atoms, auto)

lemma af_letter⇩F_range:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ) ⟹ range (af_letter⇩F φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ)}"
using af_letter⇩F_nested_prop_atoms by blast

lemma af⇩F_range:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ) ⟹ range (af⇩F φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ)}"
using af⇩F_nested_prop_atoms by blast

lemma af_letter⇩G_nested_prop_atoms:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ) ⟹ nested_prop_atoms (af_letter⇩G φ ψ ν) ⊆ nested_prop_atoms (G⇩n φ)"
by (induction ψ) (auto simp: af_letter⇩G_def, insert af_letter_nested_prop_atoms, blast+)

lemma af⇩G_nested_prop_atoms:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ) ⟹ nested_prop_atoms (af⇩G φ ψ w) ⊆ nested_prop_atoms (G⇩n φ)"
by (induction w rule: rev_induct) (insert af_letter⇩G_nested_prop_atoms, auto)

lemma af_letter⇩G_range:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ) ⟹ range (af_letter⇩G φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ)}"
using af_letter⇩G_nested_prop_atoms by blast

lemma af⇩G_range:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ) ⟹ range (af⇩G φ ψ) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ)}"
using af⇩G_nested_prop_atoms by blast

lemma af_letter⇩ν_snd_nested_prop_atoms_helper:
"snd p ∼ false⇩n ⟹ nested_prop_atoms (snd (af_letter⇩ν X p ν)) ⊆ nested_prop_atoms⇩ν (fst p) X"
"¬ snd p ∼ false⇩n ⟹ nested_prop_atoms (snd (af_letter⇩ν X p ν)) ⊆ nested_prop_atoms (snd p)"
(metis GF_advice_nested_prop_atoms⇩ν af_letter_nested_prop_atoms nested_prop_atoms⇩ν_subset dual_order.trans nested_prop_atoms⇩ν_def normalise_nested_propos)

lemma af_letter⇩ν_fst_nested_prop_atoms:
"nested_prop_atoms (fst (af_letter⇩ν X p ν)) ⊆ nested_prop_atoms (fst p)"

lemma af_letter⇩ν_snd_nested_prop_atoms:
"nested_prop_atoms (snd (af_letter⇩ν X p ν)) ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ (nested_prop_atoms (snd p))"
using af_letter⇩ν_snd_nested_prop_atoms_helper by blast

lemma af_letter⇩ν_fst_range:
"range (fst ∘ af_letter⇩ν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)}"
using af_letter⇩ν_fst_nested_prop_atoms by force

lemma af_letter⇩ν_snd_range:
"range (snd ∘ af_letter⇩ν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ nested_prop_atoms (snd p)}"
using af_letter⇩ν_snd_nested_prop_atoms by force

lemma af_letter⇩ν_range:
"range (af_letter⇩ν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ nested_prop_atoms (snd p)}"
proof -
have "range (af_letter⇩ν X p) ⊆ range (fst ∘ af_letter⇩ν X p) × range (snd ∘ af_letter⇩ν X p)"

also have "… ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ nested_prop_atoms (snd p)}"
using af_letter⇩ν_fst_range af_letter⇩ν_snd_range by blast

finally show ?thesis .
qed

lemma af⇩ν_fst_nested_prop_atoms:
"nested_prop_atoms (fst (af⇩ν X p w)) ⊆ nested_prop_atoms (fst p)"
by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms, blast)

lemma af_letter_nested_prop_atoms⇩ν:
"nested_prop_atoms⇩ν (af_letter φ ν) X ⊆ nested_prop_atoms⇩ν φ X"
by (induction φ) (simp_all add: nested_prop_atoms⇩ν_def, blast+)

lemma af⇩ν_fst_nested_prop_atoms⇩ν:
"nested_prop_atoms⇩ν (fst (af⇩ν X p w)) X ⊆ nested_prop_atoms⇩ν (fst p) X"
by (induction w rule: rev_induct) (auto, insert af_letter_nested_prop_atoms⇩ν, blast)

lemma af⇩ν_fst_range:
"range (fst ∘ af⇩ν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)}"
using af⇩ν_fst_nested_prop_atoms by fastforce

lemma af⇩ν_snd_nested_prop_atoms:
"nested_prop_atoms (snd (af⇩ν X p w)) ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ (nested_prop_atoms (snd p))"
proof (induction w arbitrary: p rule: rev_induct)
case (snoc x xs)

let ?p = "af⇩ν X p xs"

have "nested_prop_atoms (snd (af⇩ν X p (xs @ [x]))) ⊆ (nested_prop_atoms⇩ν (fst ?p) X) ∪ (nested_prop_atoms (snd ?p))"

then show ?case
using snoc af⇩ν_fst_nested_prop_atoms⇩ν by blast

lemma af⇩ν_snd_range:
"range (snd ∘ af⇩ν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ nested_prop_atoms (snd p)}"
using af⇩ν_snd_nested_prop_atoms by fastforce

lemma af⇩ν_range:
"range (af⇩ν X p) ⊆ {ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (fst p)} × {ψ. nested_prop_atoms ψ ⊆ (nested_prop_atoms⇩ν (fst p) X) ∪ nested_prop_atoms (snd p)}"
proof -
have "range (af⇩ν X p) ⊆ range (fst ∘ af⇩ν X p) × range (snd ∘ af⇩ν X p)"