Theory Syntactic_Fragments_and_Stability

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Syntactic Fragments and Stability›

theory Syntactic_Fragments_and_Stability
imports
  LTL.LTL "HOL-Library.Sublist"
begin

― ‹We use prefix and suffix on infinite words.›
hide_const Sublist.prefix Sublist.suffix

subsection ‹The fragments @{term μLTL} and @{term νLTL}

fun is_μLTL :: "'a ltln  bool"
where
  "is_μLTL truen = True"
| "is_μLTL falsen = True"
| "is_μLTL propn(_) = True"
| "is_μLTL npropn(_) = True"
| "is_μLTL (φ andn ψ) = (is_μLTL φ  is_μLTL ψ)"
| "is_μLTL (φ orn ψ) = (is_μLTL φ  is_μLTL ψ)"
| "is_μLTL (Xn φ) = is_μLTL φ"
| "is_μLTL (φ Un ψ) = (is_μLTL φ  is_μLTL ψ)"
| "is_μLTL (φ Mn ψ) = (is_μLTL φ  is_μLTL ψ)"
| "is_μLTL _ = False"

fun is_νLTL :: "'a ltln  bool"
where
  "is_νLTL truen = True"
| "is_νLTL falsen = True"
| "is_νLTL propn(_) = True"
| "is_νLTL npropn(_) = True"
| "is_νLTL (φ andn ψ) = (is_νLTL φ  is_νLTL ψ)"
| "is_νLTL (φ orn ψ) = (is_νLTL φ  is_νLTL ψ)"
| "is_νLTL (Xn φ) = is_νLTL φ"
| "is_νLTL (φ Wn ψ) = (is_νLTL φ  is_νLTL ψ)"
| "is_νLTL (φ Rn ψ) = (is_νLTL φ  is_νLTL ψ)"
| "is_νLTL _ = False"

definition μLTL :: "'a ltln set" where
  "μLTL = {φ. is_μLTL φ}"

definition νLTL :: "'a ltln set" where
  "νLTL = {φ. is_νLTL φ}"

lemma μLTL_simp[simp]:
  "φ  μLTL  is_μLTL φ"
  unfolding μLTL_def by simp

lemma νLTL_simp[simp]:
  "φ  νLTL  is_νLTL φ"
  unfolding νLTL_def by simp



subsubsection ‹Subformulas in @{term μLTL} and @{term νLTL}

fun subformulasμ :: "'a ltln  'a ltln set"
where
  "subformulasμ (φ andn ψ) = subformulasμ φ  subformulasμ ψ"
| "subformulasμ (φ orn ψ) = subformulasμ φ  subformulasμ ψ"
| "subformulasμ (Xn φ) = subformulasμ φ"
| "subformulasμ (φ Un ψ) = {φ Un ψ}  subformulasμ φ  subformulasμ ψ"
| "subformulasμ (φ Rn ψ) = subformulasμ φ  subformulasμ ψ"
| "subformulasμ (φ Wn ψ) = subformulasμ φ  subformulasμ ψ"
| "subformulasμ (φ Mn ψ) = {φ Mn ψ}  subformulasμ φ  subformulasμ ψ"
| "subformulasμ _ = {}"

fun subformulasν :: "'a ltln  'a ltln set"
where
  "subformulasν (φ andn ψ) = subformulasν φ  subformulasν ψ"
| "subformulasν (φ orn ψ) = subformulasν φ  subformulasν ψ"
| "subformulasν (Xn φ) = subformulasν φ"
| "subformulasν (φ Un ψ) = subformulasν φ  subformulasν ψ"
| "subformulasν (φ Rn ψ) = {φ Rn ψ}  subformulasν φ  subformulasν ψ"
| "subformulasν (φ Wn ψ) = {φ Wn ψ}  subformulasν φ  subformulasν ψ"
| "subformulasν (φ Mn ψ) = subformulasν φ  subformulasν ψ"
| "subformulasν _ = {}"

lemma subformulasμ_semantics:
  "subformulasμ φ = {ψ  subfrmlsn φ. ψ1 ψ2. ψ = ψ1 Un ψ2  ψ = ψ1 Mn ψ2}"
  by (induction φ) auto

lemma subformulasν_semantics:
  "subformulasν φ = {ψ  subfrmlsn φ. ψ1 ψ2. ψ = ψ1 Rn ψ2  ψ = ψ1 Wn ψ2}"
  by (induction φ) auto

lemma subformulasμ_subfrmlsn:
  "subformulasμ φ  subfrmlsn φ"
  by (induction φ) auto

lemma subformulasν_subfrmlsn:
  "subformulasν φ  subfrmlsn φ"
  by (induction φ) auto

lemma subformulasμ_finite:
  "finite (subformulasμ φ)"
  by (induction φ) auto

lemma subformulasν_finite:
  "finite (subformulasν φ)"
  by (induction φ) auto

lemma subformulasμ_subset:
  "ψ  subfrmlsn φ  subformulasμ ψ  subformulasμ φ"
  by (induction φ) auto

lemma subformulasν_subset:
  "ψ  subfrmlsn φ  subformulasν ψ  subformulasν φ"
  by (induction φ) auto

lemma subfrmlsn_μLTL:
  "φ  μLTL  subfrmlsn φ  μLTL"
  by (induction φ) auto

lemma subfrmlsn_νLTL:
  "φ  νLTL  subfrmlsn φ  νLTL"
  by (induction φ) auto

lemma subformulasμν_disjoint:
  "subformulasμ φ  subformulasν φ = {}"
  unfolding subformulasμ_semantics subformulasν_semantics
  by fastforce

lemma subformulasμν_subfrmlsn:
  "subformulasμ φ  subformulasν φ  subfrmlsn φ"
  using subformulasμ_subfrmlsn subformulasν_subfrmlsn by blast

lemma subformulasμν_card:
  "card (subformulasμ φ  subformulasν φ) = card (subformulasμ φ) + card (subformulasν φ)"
  by (simp add: subformulasμν_disjoint subformulasμ_finite subformulasν_finite card_Un_disjoint)


subsection ‹Stability›

definition "GF_singleton w φ  if w n Gn (Fn φ) then {φ} else {}"
definition "F_singleton w φ  if w n Fn φ then {φ} else {}"

declare GF_singleton_def [simp] F_singleton_def [simp]

fun 𝒢ℱ :: "'a ltln  'a set word  'a ltln set"
where
  "𝒢ℱ (φ andn ψ) w = 𝒢ℱ φ w  𝒢ℱ ψ w"
| "𝒢ℱ (φ orn ψ) w = 𝒢ℱ φ w  𝒢ℱ ψ w"
| "𝒢ℱ (Xn φ) w = 𝒢ℱ φ w"
| "𝒢ℱ (φ Un ψ) w = GF_singleton w (φ Un ψ)  𝒢ℱ φ w  𝒢ℱ ψ w"
| "𝒢ℱ (φ Rn ψ) w = 𝒢ℱ φ w  𝒢ℱ ψ w"
| "𝒢ℱ (φ Wn ψ) w = 𝒢ℱ φ w  𝒢ℱ ψ w"
| "𝒢ℱ (φ Mn ψ) w = GF_singleton w (φ Mn ψ)  𝒢ℱ φ w  𝒢ℱ ψ w"
| "𝒢ℱ _ _ = {}"

fun  :: "'a ltln  'a set word  'a ltln set"
where
  " (φ andn ψ) w =  φ w   ψ w"
| " (φ orn ψ) w =  φ w   ψ w"
| " (Xn φ) w =  φ w"
| " (φ Un ψ) w = F_singleton w (φ Un ψ)   φ w   ψ w"
| " (φ Rn ψ) w =  φ w   ψ w"
| " (φ Wn ψ) w =  φ w   ψ w"
| " (φ Mn ψ) w = F_singleton w (φ Mn ψ)   φ w   ψ w"
| " _ _ = {}"


lemma 𝒢ℱ_semantics:
  "𝒢ℱ φ w = {ψ. ψ  subformulasμ φ  w n Gn (Fn ψ)}"
  by (induction φ) force+

lemma ℱ_semantics:
  " φ w = {ψ. ψ  subformulasμ φ  w n Fn ψ}"
  by (induction φ) force+

lemma 𝒢ℱ_semantics':
  "𝒢ℱ φ w = subformulasμ φ  {ψ. w n Gn (Fn ψ)}"
  unfolding 𝒢ℱ_semantics by auto

lemma ℱ_semantics':
  " φ w = subformulasμ φ  {ψ. w n Fn ψ}"
  unfolding ℱ_semantics by auto

lemma 𝒢ℱ_ℱ_subset:
  "𝒢ℱ φ w   φ w"
  unfolding 𝒢ℱ_semantics ℱ_semantics by force


lemma 𝒢ℱ_finite:
  "finite (𝒢ℱ φ w)"
  by (induction φ) auto

lemma 𝒢ℱ_subformulasμ:
  "𝒢ℱ φ w  subformulasμ φ"
  unfolding 𝒢ℱ_semantics by force

lemma 𝒢ℱ_subfrmlsn:
  "𝒢ℱ φ w  subfrmlsn φ"
  using 𝒢ℱ_subformulasμ subformulasμ_subfrmlsn by blast

lemma 𝒢ℱ_elim:
  "ψ  𝒢ℱ φ w  w n Gn (Fn ψ)"
  unfolding 𝒢ℱ_semantics by simp

lemma 𝒢ℱ_suffix(* [simp] *):
  "𝒢ℱ φ (suffix i w) = 𝒢ℱ φ w"
proof
  show "𝒢ℱ φ w  𝒢ℱ φ (suffix i w)"
    unfolding 𝒢ℱ_semantics by auto
next
  show "𝒢ℱ φ (suffix i w)  𝒢ℱ φ w"
    unfolding 𝒢ℱ_semantics GF_Inf_many
  proof auto
    fix ψ
    assume "j. suffix (i + j) w n ψ"
    then have "j. suffix (j + i) w n ψ"
      by (simp add: algebra_simps)
    then show "j. suffix j w n ψ"
      using INFM_nat_add by blast
  qed
qed

lemma 𝒢ℱ_subset:
  "ψ  subfrmlsn φ  𝒢ℱ ψ w  𝒢ℱ φ w"
  unfolding 𝒢ℱ_semantics using subformulasμ_subset by blast


lemma ℱ_finite:
  "finite ( φ w)"
  by (induction φ) auto

lemma ℱ_subformulasμ:
  " φ w  subformulasμ φ"
  unfolding ℱ_semantics by force

lemma ℱ_subfrmlsn:
  " φ w  subfrmlsn φ"
  using ℱ_subformulasμ subformulasμ_subfrmlsn by blast

lemma ℱ_elim:
  "ψ   φ w  w n Fn ψ"
  unfolding ℱ_semantics by simp

lemma ℱ_suffix:
  " φ (suffix i w)   φ w"
  unfolding ℱ_semantics by auto

lemma ℱ_subset:
  "ψ  subfrmlsn φ   ψ w   φ w"
  unfolding ℱ_semantics using subformulasμ_subset by blast


definition "μ_stable φ w  𝒢ℱ φ w =  φ w"

lemma suffix_μ_stable:
  "i. μ_stable φ (suffix i w)"
proof -
  have "ψ  subformulasμ φ. i. suffix i w n Gn (Fn ψ)  suffix i w n Fn ψ"
    using Alm_all_GF_F by blast

  then have "i. ψ  subformulasμ φ. suffix i w n Gn (Fn ψ)  suffix i w n Fn ψ"
    using subformulasμ_finite eventually_ball_finite by fast

  then have "i. {ψ  subformulasμ φ. suffix i w n Gn (Fn ψ)} = {ψ  subformulasμ φ. suffix i w n Fn ψ}"
    by (rule MOST_mono) (blast intro: Collect_cong)

  then show ?thesis
    unfolding μ_stable_def 𝒢ℱ_semantics ℱ_semantics
    by (rule MOST_mono) simp
qed

lemma μ_stable_subfrmlsn:
  "μ_stable φ w  ψ  subfrmlsn φ  μ_stable ψ w"
proof -
  assume a1: "ψ  subfrmlsn φ" and a2: "μ_stable φ w"
  have "subformulasμ ψ  subformulasμ φ"
    using a1 by (simp add: subformulasμ_subset)
  moreover
  have "𝒢ℱ φ w =  φ w"
    using a2 by (meson μ_stable_def)
  ultimately show ?thesis
    by (metis (no_types) Un_commute ℱ_semantics' 𝒢ℱ_semantics' μ_stable_def inf_left_commute inf_sup_absorb sup.orderE)
qed

lemma μ_stable_suffix:
  "μ_stable φ w  μ_stable φ (suffix i w)"
  by (metis ℱ_suffix 𝒢ℱ_ℱ_subset 𝒢ℱ_suffix μ_stable_def subset_antisym)


definition "FG_singleton w φ  if w n Fn (Gn φ) then {φ} else {}"
definition "G_singleton w φ  if w n Gn φ then {φ} else {}"

declare FG_singleton_def [simp] G_singleton_def [simp]

fun ℱ𝒢 :: "'a ltln  'a set word  'a ltln set"
where
  "ℱ𝒢 (φ andn ψ) w = ℱ𝒢 φ w  ℱ𝒢 ψ w"
| "ℱ𝒢 (φ orn ψ) w = ℱ𝒢 φ w  ℱ𝒢 ψ w"
| "ℱ𝒢 (Xn φ) w = ℱ𝒢 φ w"
| "ℱ𝒢 (φ Un ψ) w = ℱ𝒢 φ w  ℱ𝒢 ψ w"
| "ℱ𝒢 (φ Rn ψ) w = FG_singleton w (φ Rn ψ)  ℱ𝒢 φ w  ℱ𝒢 ψ w"
| "ℱ𝒢 (φ Wn ψ) w = FG_singleton w (φ Wn ψ)  ℱ𝒢 φ w  ℱ𝒢 ψ w"
| "ℱ𝒢 (φ Mn ψ) w = ℱ𝒢 φ w  ℱ𝒢 ψ w"
| "ℱ𝒢 _ _ = {}"

fun 𝒢 :: "'a ltln  'a set word  'a ltln set"
where
  "𝒢 (φ andn ψ) w = 𝒢 φ w  𝒢 ψ w"
| "𝒢 (φ orn ψ) w = 𝒢 φ w  𝒢 ψ w"
| "𝒢 (Xn φ) w = 𝒢 φ w"
| "𝒢 (φ Un ψ) w = 𝒢 φ w  𝒢 ψ w"
| "𝒢 (φ Rn ψ) w = G_singleton w (φ Rn ψ)  𝒢 φ w  𝒢 ψ w"
| "𝒢 (φ Wn ψ) w = G_singleton w (φ Wn ψ)  𝒢 φ w  𝒢 ψ w"
| "𝒢 (φ Mn ψ) w = 𝒢 φ w  𝒢 ψ w"
| "𝒢 _ _ = {}"


lemma ℱ𝒢_semantics:
  "ℱ𝒢 φ w = {ψ  subformulasν φ. w n Fn (Gn ψ)}"
  by (induction φ) force+

lemma 𝒢_semantics:
  "𝒢 φ w  {ψ  subformulasν φ. w n Gn ψ}"
  by (induction φ) force+

lemma ℱ𝒢_semantics':
  "ℱ𝒢 φ w = subformulasν φ  {ψ. w n Fn (Gn ψ)}"
  unfolding ℱ𝒢_semantics by auto

lemma 𝒢_semantics':
  "𝒢 φ w = subformulasν φ  {ψ. w n Gn ψ}"
  unfolding 𝒢_semantics by auto

lemma 𝒢_ℱ𝒢_subset:
  "𝒢 φ w  ℱ𝒢 φ w"
  unfolding 𝒢_semantics ℱ𝒢_semantics by force

lemma ℱ𝒢_finite:
  "finite (ℱ𝒢 φ w)"
  by (induction φ) auto

lemma ℱ𝒢_subformulasν:
  "ℱ𝒢 φ w  subformulasν φ"
  unfolding ℱ𝒢_semantics by force

lemma ℱ𝒢_subfrmlsn:
  "ℱ𝒢 φ w  subfrmlsn φ"
  using ℱ𝒢_subformulasν subformulasν_subfrmlsn by blast

lemma ℱ𝒢_elim:
  "ψ  ℱ𝒢 φ w  w n Fn (Gn ψ)"
  unfolding ℱ𝒢_semantics by simp

lemma ℱ𝒢_suffix:
  "ℱ𝒢 φ (suffix i w) = ℱ𝒢 φ w"
proof
  show "ℱ𝒢 φ (suffix i w)  ℱ𝒢 φ w"
    unfolding ℱ𝒢_semantics by auto
next
  show "ℱ𝒢 φ w  ℱ𝒢 φ (suffix i w)"
    unfolding ℱ𝒢_semantics FG_Alm_all
  proof auto
    fix ψ
    assume "j. suffix j w n ψ"
    then have "j. suffix (j + i) w n ψ"
      using MOST_nat_add by meson
    then show "j. suffix (i + j) w n ψ"
      by (simp add: algebra_simps)
  qed
qed

lemma ℱ𝒢_subset:
  "ψ  subfrmlsn φ  ℱ𝒢 ψ w  ℱ𝒢 φ w"
  unfolding ℱ𝒢_semantics using subformulasν_subset by blast


lemma 𝒢_finite:
  "finite (𝒢 φ w)"
  by (induction φ) auto

lemma 𝒢_subformulasν:
  "𝒢 φ w  subformulasν φ"
  unfolding 𝒢_semantics by force

lemma 𝒢_subfrmlsn:
  "𝒢 φ w  subfrmlsn φ"
  using 𝒢_subformulasν subformulasν_subfrmlsn by blast

lemma 𝒢_elim:
  "ψ  𝒢 φ w  w n Gn ψ"
  unfolding 𝒢_semantics by simp

lemma 𝒢_suffix:
  "𝒢 φ w  𝒢 φ (suffix i w)"
  unfolding 𝒢_semantics by auto

lemma 𝒢_subset:
  "ψ  subfrmlsn φ  𝒢 ψ w  𝒢 φ w"
  unfolding 𝒢_semantics using subformulasν_subset by blast


definition "ν_stable φ w  ℱ𝒢 φ w = 𝒢 φ w"

lemma suffix_ν_stable:
  "j. ν_stable φ (suffix j w)"
proof -
  have "ψ  subformulasν φ. i. suffix i w n Fn (Gn ψ)  suffix i w n Gn ψ"
    using Alm_all_FG_G by blast

  then have "i. ψ  subformulasν φ. suffix i w n Fn (Gn ψ)  suffix i w n Gn ψ"
    using subformulasν_finite eventually_ball_finite by fast

  then have "i. {ψ  subformulasν φ. suffix i w n Fn (Gn ψ)} = {ψ  subformulasν φ. suffix i w n Gn ψ}"
    by (rule MOST_mono) (blast intro: Collect_cong)

  then show ?thesis
    unfolding ν_stable_def ℱ𝒢_semantics 𝒢_semantics
    by (rule MOST_mono) simp
qed

lemma ν_stable_subfrmlsn:
  "ν_stable φ w  ψ  subfrmlsn φ  ν_stable ψ w"
proof -
  assume a1: "ψ  subfrmlsn φ" and a2: "ν_stable φ w"
  have "subformulasν ψ  subformulasν φ"
    using a1 by (simp add: subformulasν_subset)
  moreover
  have "ℱ𝒢 φ w = 𝒢 φ w"
    using a2 by (meson ν_stable_def)
  ultimately show ?thesis
    by (metis (no_types) Un_commute 𝒢_semantics' ℱ𝒢_semantics' ν_stable_def inf_left_commute inf_sup_absorb sup.orderE)
qed

lemma ν_stable_suffix:
  "ν_stable φ w  ν_stable φ (suffix i w)"
  by (metis ℱ𝒢_suffix 𝒢_ℱ𝒢_subset 𝒢_suffix ν_stable_def antisym_conv)


subsection ‹Definitions with Lists for Code Export›

text ‹The μ›- and ν›-subformulas as lists:›

fun subformulasμ_list :: "'a ltln  'a ltln list"
where
  "subformulasμ_list (φ andn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (φ orn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (Xn φ) = subformulasμ_list φ"
| "subformulasμ_list (φ Un ψ) = List.insert (φ Un ψ) (List.union (subformulasμ_list φ) (subformulasμ_list ψ))"
| "subformulasμ_list (φ Rn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (φ Wn ψ) = List.union (subformulasμ_list φ) (subformulasμ_list ψ)"
| "subformulasμ_list (φ Mn ψ) = List.insert (φ Mn ψ) (List.union (subformulasμ_list φ) (subformulasμ_list ψ))"
| "subformulasμ_list _ = []"

fun subformulasν_list :: "'a ltln  'a ltln list"
where
  "subformulasν_list (φ andn ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list (φ orn ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list (Xn φ) = subformulasν_list φ"
| "subformulasν_list (φ Un ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list (φ Rn ψ) = List.insert (φ Rn ψ) (List.union (subformulasν_list φ) (subformulasν_list ψ))"
| "subformulasν_list (φ Wn ψ) = List.insert (φ Wn ψ) (List.union (subformulasν_list φ) (subformulasν_list ψ))"
| "subformulasν_list (φ Mn ψ) = List.union (subformulasν_list φ) (subformulasν_list ψ)"
| "subformulasν_list _ = []"

lemma subformulasμ_list_set:
  "set (subformulasμ_list φ) = subformulasμ φ"
  by (induction φ) auto

lemma subformulasν_list_set:
  "set (subformulasν_list φ) = subformulasν φ"
  by (induction φ) auto

lemma subformulasμ_list_distinct:
  "distinct (subformulasμ_list φ)"
  by (induction φ) auto

lemma subformulasν_list_distinct:
  "distinct (subformulasν_list φ)"
  by (induction φ) auto

lemma subformulasμ_list_length:
  "length (subformulasμ_list φ) = card (subformulasμ φ)"
  by (metis subformulasμ_list_set subformulasμ_list_distinct distinct_card)

lemma subformulasν_list_length:
  "length (subformulasν_list φ) = card (subformulasν φ)"
  by (metis subformulasν_list_set subformulasν_list_distinct distinct_card)


text ‹
  We define the list of advice sets as the product of all subsequences
  of the μ›- and ν›-subformulas of a formula.
›

definition advice_sets :: "'a ltln  ('a ltln list × 'a ltln list) list"
where
  "advice_sets φ = List.product (subseqs (subformulasμ_list φ)) (subseqs (subformulasν_list φ))"

lemma subset_subseq:
  "X  set ys  (xs. X = set xs  subseq xs ys)"
  by (metis (no_types, lifting) Pow_iff image_iff in_set_subseqs subseqs_powset)

lemma subseqs_subformulasμ_list:
  "X  subformulasμ φ  (xs. X = set xs  xs  set (subseqs (subformulasμ_list φ)))"
  by (metis subset_subseq subformulasμ_list_set in_set_subseqs)

lemma subseqs_subformulasν_list:
  "Y  subformulasν φ  (ys. Y = set ys  ys  set (subseqs (subformulasν_list φ)))"
  by (metis subset_subseq subformulasν_list_set in_set_subseqs)

lemma advice_sets_subformulas:
  "X  subformulasμ φ  Y  subformulasν φ  (xs ys. X = set xs  Y = set ys  (xs, ys)  set (advice_sets φ))"
  unfolding advice_sets_def set_product subseqs_subformulasμ_list subseqs_subformulasν_list by blast

(* TODO add to HOL/List.thy *)
lemma subseqs_not_empty:
  "subseqs xs  []"
  by (metis empty_iff list.set(1) subseqs_refl)

(* TODO add to HOL/List.thy *)
lemma product_not_empty:
  "xs  []  ys  []  List.product xs ys  []"
  by (induction xs) simp_all

lemma advice_sets_not_empty:
  "advice_sets φ  []"
  unfolding advice_sets_def using subseqs_not_empty product_not_empty by blast

lemma advice_sets_length:
  "length (advice_sets φ)  2 ^ card (subfrmlsn φ)"
  unfolding advice_sets_def length_product length_subseqs subformulasμ_list_length subformulasν_list_length power_add[symmetric]
  by (metis Suc_1 card_mono lessI power_increasing_iff subformulasμν_card subformulasμν_subfrmlsn subfrmlsn_finite)

lemma advice_sets_element_length:
  "(xs, ys)  set (advice_sets φ)  length xs  card (subfrmlsn φ)"
  "(xs, ys)  set (advice_sets φ)  length ys  card (subfrmlsn φ)"
  unfolding advice_sets_def set_product
  by (metis SigmaD1 card_mono in_set_subseqs list_emb_length order_trans subformulasμ_list_length subformulasμ_subfrmlsn subfrmlsn_finite)
     (metis SigmaD2 card_mono in_set_subseqs list_emb_length order_trans subformulasν_list_length subformulasν_subfrmlsn subfrmlsn_finite)

lemma advice_sets_element_subfrmlsn:
  "(xs, ys)  set (advice_sets φ)  set xs  subformulasμ φ"
  "(xs, ys)  set (advice_sets φ)  set ys  subformulasν φ"
  unfolding advice_sets_def set_product
  by (meson SigmaD1 subseqs_subformulasμ_list)
     (meson SigmaD2 subseqs_subformulasν_list)

end