Theory MuddyChildren

theory MuddyChildren
imports Main DEAKDerivedRules "calculus/src/isabelle/DEAK_SE" NatToString
begin

(*
Implements and follows closely the proof of Proposition 24 in (Ma-Palmigiano-Sadrzadeh, 2014), 
referred to in the comments below as [MPS].
We consider classical logic and define clean as the negation of dirty.
*)

(* as upto is not defined for nats in isabelle core theories, we introduce a sugar notation for constructing a list of nats from x to y: [[x .. y]] *)
fun upto' :: "nat ⇒ nat ⇒ nat list" ("[[_ .. _]]") where
"upto' x 0 = (if x = 0 then [0] else [])" |
"upto' x (Suc y) = (if x ≤ (Suc y) then (if x = Suc y then [Suc y] else (Suc y) # (upto' x y)) else [])"

lemma upto'_simp1[simp]: "x ≤ y ⟹ set ([[x .. y]]) = {x..y}"
by (induct y, auto)

lemma upto'_simp2[simp]: "x > y ⟹ set ([[x .. y]]) = {x..y}"
by (induct y, auto)

(* E f := ⋀n i=1 fboxK i f. The intended meaning of the defined connective E is ‘Everybody knows’ *)
fun E :: "nat ⇒ Formula ⇒ Formula" where
"E 0 formula = ⊤⇩F" |
"E (Suc x) formula = (fboxK⇩F (`Suc x`) formula) ∧⇩F (E x formula)"

lemma E_der_simp: 
  fixes x A
  shows "⋀i. 0 < i ∧ i ≤ (Suc x) ⟹ loc ⊢d ( E (Suc x) A )⇩S ⊢⇩S ( fboxK⇩F `i` A )⇩S"
proof(induct x)
case 0 
  then have i_eq_1: "i = Suc 0" by simp
  show ?case
  apply (subst i_eq_1)+
  unfolding E.simps
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  by (rule Id)
next
case (Suc x)
  thus ?case
  proof (cases "i ≤ Suc x")
  case goal1 
    then have assm: "loc ⊢d E (Suc x) A ⇩S ⊢⇩S fboxK⇩F `i` A ⇩S" by simp
    thus ?case 
    apply (subst E.simps)
    apply (rule_tac derivable.And_L)
    apply (rule_tac derivable.Comma_impL_disp2)
    apply (rule_tac derivable.W_impL_L)
    by simp
  next
  case goal2 
    then have assm: "i = Suc (Suc x)" by simp
    thus ?case
    apply (subst E.simps)
    apply (rule_tac derivable.And_L)
    apply (rule_tac derivable.Comma_impR_disp2)
    apply (rule_tac derivable.W_impR_R)
    apply (subst assm)
    by (rule Id)
  qed
qed

lemma E_der_simp2:
  assumes "⋀ag. LAgent ag ∈ set loc"
  shows "⋀x A. loc ⊢d ( E (Suc x)⇧y A )⇩S ⊢⇩S ( A )⇩S"
apply(induct y)
unfolding k_apply.simps
apply (rule Id)
apply (subst E.simps)
apply (rule_tac derivable.And_L)
apply (rule_tac derivable.Comma_impR_disp2)
apply (rule_tac derivable.W_impR_R)
apply (rule_tac a="`Suc x`" in derivable.Refl_ForwK)
using assms apply simp
apply (rule_tac derivable.FboxK_L)
by simp

definition father :: "nat ⇒ Formula" where
"father n = ⋁⇩F map (Formula_Atprop ∘ nat_to_string) [[1 .. n]]"

(* vision expresses the fact that every child knows whether each other child is clean or dirty *)
fun vision_aux :: "nat ⇒ nat ⇒ Formula list" where
"vision_aux _ 0 = []" |
"vision_aux m (Suc n) = (
  ((`m` ⇩F) →⇩F (fboxK⇩F (`Suc n`) (`m` ⇩F))) ∧⇩F 
  (((`m` ⇩F) →⇩F ⊥⇩F) →⇩F (fboxK⇩F (`Suc n`) ((`m` ⇩F) →⇩F ⊥⇩F)))
)
#
(
  (((`Suc n`) ⇩F) →⇩F (fboxK⇩F `m` ((`Suc n`) ⇩F))) ∧⇩F 
  ((((`Suc n`) ⇩F) →⇩F ⊥⇩F) →⇩F (fboxK⇩F `m` (((`Suc n`) ⇩F) →⇩F ⊥⇩F)))
)
# vision_aux m n"

fun vision' :: "nat ⇒ Formula list" where
"vision' 0 = []" |
"vision' (Suc x) = (vision_aux (Suc x) x) @ (vision' x)"

definition vision :: "nat ⇒ Formula" where
"vision x = ⋀⇩F (vision' x)"

lemma vision_aux_contains1 :
  assumes "0 < i ∧ i < (Suc x)"
  shows "⋀ ii. 0 < ii ∧ ii < i ⟹ (
   (((`Suc x`) ⇩F) →⇩F (fboxK⇩F `ii` ((`Suc x`) ⇩F))) ∧⇩F 
   ((((`Suc x`) ⇩F) →⇩F ⊥⇩F) →⇩F (fboxK⇩F `ii` (((`Suc x`) ⇩F) →⇩F ⊥⇩F)))
  )
   ∈ set (vision_aux (Suc x) i)"
using assms proof (induction x i rule: vision_aux.induct)
case 1 thus ?case by auto
next
case (2 m n)
  show ?case
  apply(cases "ii < n")
  proof -
  case goal1
    with 2 show ?case by simp
  next
  case goal2
    then have "ii ≥ n" by simp
    from 2 have "ii ≤ n" by simp
    then have i_def: "ii = n" by (simp add: `n ≤ ii` dual_order.antisym)
    then obtain n' where n'_def: "n = Suc n'" by (metis "2.prems"(1) Suc_pred)
    show ?case 
    unfolding i_def vision_aux.simps
    apply(subst (9) n'_def)
    unfolding vision_aux.simps using n'_def by simp
  qed
qed

lemma vision_aux_contains2 :
  assumes "0 < i ∧ i < (Suc x)"
  shows "⋀ ii. 0 < ii ∧ ii < i ⟹ (
   ((`ii` ⇩F) →⇩F (fboxK⇩F (`Suc x`) (`ii` ⇩F))) ∧⇩F 
   (((`ii` ⇩F) →⇩F ⊥⇩F) →⇩F (fboxK⇩F (`Suc x`) ((`ii` ⇩F) →⇩F ⊥⇩F)))
  )
   ∈ set (vision_aux (Suc x) i)"
using assms proof (induction x i rule: vision_aux.induct)
case 1 thus ?case by auto
next
case (2 m n)
  show ?case
  apply(cases "ii < n")
  proof -
  case goal1
    with 2 show ?case by simp
  next
  case goal2
    then have "ii ≥ n" by simp
    from 2 have "ii ≤ n" by simp
    then have i_def: "ii = n" by (simp add: `n ≤ ii` dual_order.antisym)
    then obtain n' where n'_def: "n = Suc n'" by (metis "2.prems"(1) Suc_pred)
    show ?case 
    unfolding i_def vision_aux.simps
    apply(subst (9) n'_def)
    unfolding vision_aux.simps using n'_def by simp
  qed
qed

lemma vision_contains :
  fixes i j dirty_children num_of_children
  assumes "0 < i ∧ i ≤ num_of_children" "0 < j ∧ j ≤ num_of_children"
  and "i ≠ j"
  shows "((`j` ⇩F) →⇩F (fboxK⇩F `i` (`j` ⇩F))) ∧⇩F 
  (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F (fboxK⇩F `i` ((`j` ⇩F) →⇩F ⊥⇩F))) ∈ set (vision' num_of_children)"
using assms apply (induct num_of_children)
apply simp
proof -
case goal1 
  note g1 = goal1
  show ?case
  proof (cases "i ≤ num_of_children" ; cases "j ≤ num_of_children")
  case goal1 
    with g1 have "((`j` ⇩F) →⇩F fboxK⇩F `i` `j` ⇩F) ∧⇩F (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `i` (`j` ⇩F) →⇩F ⊥⇩F)
    ∈ set (vision' num_of_children)" by simp
    thus ?case unfolding vision'.simps by simp
  next
  case goal2 
    with g1 have j_def: "j = Suc num_of_children" by simp
    with g1 goal2 obtain num' where num'_def: "num_of_children = Suc num'" using Suc_pred less_le_trans by metis
    then have "((`Suc num_of_children` ⇩F) →⇩F fboxK⇩F `i` `Suc num_of_children` ⇩F) ∧⇩F
    (((`Suc num_of_children` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `i` (`Suc num_of_children` ⇩F) →⇩F ⊥⇩F)
    ∈ set (vision_aux (Suc num_of_children) num_of_children)" using g1 goal2 vision_aux_contains1 
    by (metis le_less lessI list.set_intros(1) vision_aux.simps(2) zero_less_Suc)
    thus ?case unfolding j_def vision'.simps by simp
  next
  case goal3 
    with g1 have i_def: "i = Suc num_of_children" by simp
    with g1 goal3 obtain num' where num'_def: "num_of_children = Suc num'" using Suc_pred less_le_trans by metis
    then have "((`j` ⇩F) →⇩F fboxK⇩F `Suc num_of_children` `j` ⇩F) ∧⇩F
    (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `Suc num_of_children` (`j` ⇩F) →⇩F ⊥⇩F)
    ∈ set (vision_aux (Suc num_of_children) num_of_children)" using g1 goal3 vision_aux_contains2
    by (metis le_less lessI list.set_intros(1) list.set_intros(2) vision_aux.simps(2) zero_less_Suc) 
    thus ?case unfolding i_def vision'.simps by simp
  next
  case goal4 
    with g1 have False by simp
    thus ?case ..
  qed
qed

(* no expresses the ignorance of the children about their own status *)
fun no :: "nat ⇒ Formula" where
"no 0 = ⊤⇩F"|
"no (Suc x) = ( ( fdiamK⇩F (`Suc x`) (`Suc x`) ⇩F )
  ∧⇩F ( fdiamK⇩F (`Suc x`) (( (`Suc x` ) ⇩F) →⇩F ⊥⇩F ) ) ) ∧⇩F ( no x)"

lemma no_imp: 
  fixes loc
  assumes "0 < i ∧ i ≤ Suc( x)"
  shows " loc ⊢d ( no (Suc x) ) ⇩S ⊢⇩S ( ( fdiamK⇩F `i` (`i` ) ⇩F ) ∧⇩F ( fdiamK⇩F `i` ( ( (`i` ) ⇩F) →⇩F ⊥⇩F )) ) ⇩S "
using assms apply(induction x)
apply (subst no.simps)+
proof -
case goal1
  have i0: "i = Suc 0" by (simp add: Suc_leI goal1 le_antisym)
  show ?case
  apply(subst i0)+
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  by (rule Id)
next
case goal2
  show ?case
  apply (subst no.simps)
  apply(cases "i≤ (Suc x)")
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  using goal2(1) goal2(2) apply blast

  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  using Id goal2(2) le_SucE by blast
qed

(* the first parameter n encodes the number of children - 
   the second parameter J encodes the list of dirty children which is a subset of {1..n} *)
definition dirty :: "nat ⇒ nat list ⇒ Formula " where
"dirty n J = (if ∀j ∈ (set J). n ≥ j ∧ j > 0 then 
  ⋀⇩F (map (Formula_Atprop ∘ nat_to_string) J) @
     (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) (filter (λx. x ∉ set J) [[1 .. n]])) else ⊤⇩F )"

lemma dirty_vision_der:
  fixes k n J J' j
assumes "0 ≤ (Suc k) ∧ (Suc k) ≤ n" 
  and "set J ⊆ {1..n}"
  and "j ∈ set J"
  and "set J' ≡ set J - {j}"
  and cut: "⋀f. CutFormula f ∈ set loc"
shows "loc ⊢d (dirty n J ⇩S) ;⇩S (vision n ⇩S) ⊢⇩S (fboxK⇩F `j` (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F dirty n J')) ⇩S"
proof -
case goal1
  from assms have cond: "∀j∈set J. j ≤ n ∧ 0 < j" "∀j∈set J'. j ≤ n ∧ 0 < j" by auto

  have 1: "loc ⊢d (⋀⇩F ((map (Formula_Atprop ∘ nat_to_string) J') @ (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J]))) ⇩S ⊢⇩S 
    ((`j` ⇩F) →⇩F ⊥⇩F) →⇩F (⋀⇩F ((map (Formula_Atprop ∘ nat_to_string) J') @ (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J']))) ⇩S"
  apply(rule_tac f= "(⋀⇩F ((map (Formula_Atprop ∘ nat_to_string) J'))) ∧⇩F 
    ((⋀⇩F (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])))" in derivable.SingleCut)
  using cut apply blast
  apply(rule_tac conj_unfold_2)
  using cut apply blast
  apply(rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply(rule_tac f= "(⋀⇩F ((map (Formula_Atprop ∘ nat_to_string) J'))) ∧⇩F 
    ((⋀⇩F (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J'])))" in derivable.SingleCut)
  using cut apply blast
  defer
  apply(rule_tac conj_unfold_2b)
  using cut apply blast
  apply (rule_tac derivable.Comma_impR_disp2)
  apply(rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp)
  apply(rule_tac derivable.E_L)
  apply(rule_tac derivable.A_L2)
  apply(rule_tac derivable.And_R)
  defer
  apply(rule_tac conj_der2)
  using cut apply simp
  apply(rule_tac Id)
  using assms apply auto[1]
  apply(rule_tac conj_der1b)
  apply rule
  proof -
  case goal1 thus ?case
    apply (cases "f ∈ set (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])")
    apply (rule_tac derivable.Comma_impR_disp2)
    apply (rule_tac derivable.W_impR_R)
    apply(rule_tac f=f in conj_der1)
    apply(rule Id)
    apply blast
    proof -
    case goal1
      then have 0: "f ∈ set (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J']) - set (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])" using Set.DiffI by blast
      from assms have "set [[1 ..n ]] = {1..n}" by simp
      with assms have 1: "set [x← [[1 .. n]] . x ∉ set J'] = {1..n} - (set J - {j})" and 2: "set [x← [[1 .. n]] . x ∉ set J] = {1..n} - (set J)" by auto
      
      
      from assms have "set J - {j} ⊆ {1..n}" "{j} ⊆ {1..n}" by auto
      with assms(2,3) have 3: "set [x← [[1 .. n]] . x ∉ set J'] - set [x← [[1 .. n]] . x ∉ set J] = {j}"
      apply(subst 1)
      apply(subst 2)
      by auto
      
      have "set (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J']) - set (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J]) =
      image ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) ((set [x← [[1 .. n]] . x ∉ set J']) - set [x← [[1 .. n]] . x ∉ set J])"
      proof -
        have "∀F f. F ≠ {} ∨ (f :: Formula) ∉ F"
          by blast
        hence f1: "set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J']) - set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J]) ≠ {}"
          using "0" by blast
        have f2: "set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J']) - set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J]) - insert (((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) j) (((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) ` {}) = {}"
          by (metis (no_types) Diff_eq_empty_iff `set [x← [[1 .. n]] . x ∉ set J'] - set [x← [[1 .. n]] . x ∉ set J] = {j}` image_diff_subset image_insert image_set)
        hence f3: "insert (((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) j) (set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J']) - set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J]) - {((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) j}) = ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) ` {j}"
          by blast
        have "((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) j ∈ set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J']) - set (map ((λcs. (cs ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [n← [[1 .. n]] . n ∉ set J])"
          using f2 f1 by blast
        thus ?thesis
          using f3 by (metis `set [x← [[1 .. n]] . x ∉ set J'] - set [x← [[1 .. n]] . x ∉ set J] = {j}` insert_Diff)
      qed
      
      with 0 3 have f_def: "f = (`j` ⇩F) →⇩F ⊥⇩F" by (metis (no_types, lifting) comp_apply imageE singletonD)
      thus ?case
      unfolding f_def
      apply (rule_tac derivable.Comma_impL_disp2)
      apply (rule_tac derivable.W_impL_L)
      by (rule_tac Id)
    qed
  qed

  have subst1: "map ((λx. fboxK⇩F `j` x ⇩F) ∘ nat_to_string) J' @ map ((λx. fboxK⇩F `j` ((x ⇩F) →⇩F ⊥⇩F)) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J] = 
    map (λx. fboxK⇩F `j` x) (map ((λx. x ⇩F) ∘ nat_to_string) J' @ map ((λx. ((x ⇩F) →⇩F ⊥⇩F)) ∘ nat_to_string) [x← [[1 .. n]] .  x ∉ set J])" by simp

  have subst2: "((λx. ((x ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) = ((λx. ((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F) →⇩F ⊥⇩F))" by (meson comp_apply)
  have subst3: "((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) = (λx. (`x` ⇩F) →⇩F ⊥⇩F)" by auto
  have subst4: "((λx. fboxK⇩F `j` ((x ⇩F) →⇩F ⊥⇩F)) ∘ nat_to_string) = (λx. fboxK⇩F `j` ((`x` ⇩F) →⇩F ⊥⇩F))" by (meson comp_apply)
  have subst5: "((λx. fboxK⇩F `j` x ⇩F) ∘ nat_to_string) = (λx. fboxK⇩F `j` `x` ⇩F)" by (meson comp_apply)

  have "loc ⊢d ((⋀⇩F ((map (Formula_Atprop ∘ nat_to_string) J) @ (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J]))) ⇩S) ;⇩S (vision n ⇩S) ⊢⇩S 
    (fboxK⇩F `j` (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F (⋀⇩F ((map (Formula_Atprop ∘ nat_to_string) J') @ (map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J']))))) ⇩S"
  apply(rule_tac f ="fboxK⇩F `j` (⋀⇩F map (Formula_Atprop ∘ nat_to_string) J' @ map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])" in SingleCut)
  using cut apply blast
  defer
  using FboxK_L FboxK_R 1 apply blast
  apply(rule_tac f ="(⋀⇩F map ((λx. fboxK⇩F `j` (x ⇩F)) ∘ nat_to_string) J' @ map ((λx. fboxK⇩F `j` ((x ⇩F) →⇩F ⊥⇩F)) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])" in SingleCut)
  using cut apply simp
  defer
  apply(subst subst1)
  apply(rule_tac conj_box_distrib)
  using cut apply simp
  apply(rule_tac f ="(⋀⇩F map ((λx. fboxK⇩F `j` (x ⇩F)) ∘ nat_to_string) J') ∧⇩F (⋀⇩F map ((λx. fboxK⇩F `j` ((x ⇩F) →⇩F ⊥⇩F)) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])" in SingleCut)
  using cut apply simp
  defer
  apply(rule_tac conj_unfold_2b)
  using cut apply simp
  apply (rule_tac derivable.Comma_impL_disp2)
  apply(rule_tac f ="(⋀⇩F map (Formula_Atprop ∘ nat_to_string) J) ∧⇩F (⋀⇩F map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J])" in SingleCut)
  using cut apply simp
  apply(rule_tac conj_unfold_2)
  using cut apply simp
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.A_L2)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.A_L)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.A_L2)
  apply (rule_tac derivable.And_R)

  apply(rule_tac f ="(⋀⇩F map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. n]] . x ∉ set J]) ∧⇩F (⋀⇩F map ((λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F)) ∧⇩F (((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` ((`x` ⇩F) →⇩F ⊥⇩F)))) [x← [[1 .. n]] . x ∉ set J])" in SingleCut)
  using cut apply simp
  apply (rule_tac derivable.And_R)
  defer
  apply (rule Id)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)

  apply(rule_tac f ="(⋀⇩F map ((λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F)))) [x← [[1 .. n]] . x ∉ set J]) ∧⇩F (⋀⇩F map (λx. ((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` ((`x` ⇩F) →⇩F ⊥⇩F)) [x← [[1 .. n]] . x ∉ set J])" in SingleCut)
  using cut apply simp
  apply(rule conj_fold)
  using cut apply simp
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply (rule_tac derivable.Comma_impR_disp)

  apply(subst subst3)
  apply(subst subst4)
  
  apply(rule_tac conj_impl_fold)
  using cut apply simp

  apply(rule_tac f ="(⋀⇩F map (λx. (`x` ⇩F)) J') ∧⇩F (⋀⇩F map ((λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F)) ∧⇩F (((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` ((`x` ⇩F) →⇩F ⊥⇩F)))) J')" in SingleCut)
  using cut apply simp
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.And_R)
  defer
  apply (rule_tac conj_der2)
  using cut apply simp
  apply (rule Id)
  using assms apply auto[1]
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)

  apply(rule_tac f ="(⋀⇩F map ((λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F)))) J') ∧⇩F (⋀⇩F map (λx. ((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` ((`x` ⇩F) →⇩F ⊥⇩F)) J')" in SingleCut)
  using cut apply simp
  apply(rule conj_fold)
  using cut apply simp
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  apply (rule_tac derivable.Comma_impR_disp)

  apply(subst subst5)
  apply(rule_tac conj_impl_fold)
  using cut apply simp
  unfolding vision_def
  apply(rule_tac conj_der1b)
  apply rule
  apply(rule_tac conj_der1)
  apply(rule Id)
  defer
  apply(rule_tac conj_der1b)
  apply rule
  apply(rule_tac conj_der1)
  apply(rule Id)
  proof -
  case goal1 
    then have 0: "f ∈ image (λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` `x` ⇩F) ∧⇩F (((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F) →⇩F ⊥⇩F)) (set J')" by (metis list.set_map)
    from assms have "∀x ∈ set J'. 0 < x ∧ x ≤ n" "∀x ∈ set J'. x ≠ j" by auto
    then have "∀x ∈ (set J'). ((`x` ⇩F) →⇩F fboxK⇩F `j` `x` ⇩F) ∧⇩F (((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F) →⇩F ⊥⇩F) ∈ set (vision' n)" by (metis (no_types, lifting) assms(3) cond(1) vision_contains)
    with 0 show ?case by blast
  next
  case goal2
    then have 0: "f ∈ image (λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` `x` ⇩F) ∧⇩F (((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F) →⇩F ⊥⇩F)) (set [x← [[1 .. n]] . x ∉ set J])" by (metis list.set_map)
    from assms have "∀x ∈ set [x← [[1 .. n]] . x ∉ set J]. 0 < x ∧ x ≤ n" "∀x ∈ set [x← [[1 .. n]] . x ∉ set J]. x ≠ j" 
    apply (metis One_nat_def Suc_eq_plus1 atLeastAtMost_iff atLeastatMost_empty_iff discrete filter_is_subset insert_Diff insert_not_empty subsetCE upto'_simp1)
    using assms(3) by auto
    then have "∀x ∈ set [x← [[1 .. n]] . x ∉ set J]. ((`x` ⇩F) →⇩F fboxK⇩F `j` `x` ⇩F) ∧⇩F (((`x` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`x` ⇩F) →⇩F ⊥⇩F) ∈ set (vision' n)" by (metis (no_types, lifting) assms(3) cond(1) vision_contains)
    with 0 show ?case by blast
  qed

  thus ?case unfolding dirty_def using cond by simp
qed

definition preFormula_father :: "nat ⇒ Locale" where
"preFormula_father n = PreFormula (''father''@`n`) (father n)"

definition preFormula_no :: "nat ⇒ Locale" where
"preFormula_no n = PreFormula (''no''@`n`) (no n)"

lemma dirtyChildren:
  fixes J::"nat list" and j and n
  assumes "(Suc k) ≤ (Suc n)"
  and "set J ⊆ {1..Suc n}"
  and "card (set J) = Suc k"
  and "j ∈ set J"  
  assumes preFather: "⋀n. preFormula_father (Suc n) ∈ set loc"
  and preNo: "⋀n. preFormula_no (Suc n) ∈ set loc"
  and rel_refl: "RelAKA rel ∈ set loc" "⋀ alpha a. rel alpha a = ([alpha]::Action list)" 
  and cut: "⋀f. CutFormula f ∈ set loc"
  and agent: "⋀agent. LAgent agent ∈ set loc"
  shows "loc ⊢d ((dirty (Suc n) J) ∧⇩F (k_apply (E (Suc n)) (Suc k) (vision (Suc n))))⇩S ⊢⇩S 
    (fboxA⇩F (''father'' @ `Suc n`) (k_apply (Formula_FboxA (''no'' @ `Suc n`)) k (fboxK⇩F `j` `j` ⇩F)) )⇩S"
using assms(1,2,3,4)
proof(induct k arbitrary:j J)
case 0 (* k=0, hence there is Suc k = 1 dirty child, called j, J={j} *)
  then have J_contains: "set J = {j}" using card_eq_SucD by fastforce
  
  have set_eq: "{1..Suc n} - {j} = set ([x ←  [[1 .. Suc n]]. x≠j])" by auto


  
  have red_ax_1: "loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n)) ⇩S ⊢⇩S 
    ((father (Suc n) ⇩S) →⇩S (forwK⇩S `j` (father (Suc n) ⇩S) →⇩S (`j` ⇩F ⇩S))) ⟹ 
    loc ⊢d (dirty (Suc n) J ∧⇩F  E (Suc n) ⇧Suc 0 vision (Suc n)) ⇩S ⊢⇩S 
    (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧0 fboxK⇩F `j` (`j` ⇩F) )⇩S"
  apply (subst k_apply.simps(1))
  (* begin proof red_ax_1.cs *)
  apply (rule_tac derivable.FboxA_R)
  apply (rule_tac derivable.Back_forw_A2)
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.Back_forw_A)
  apply (rule_tac derivable.Reduce_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.I_impL2)
  apply (rule_tac derivable.Bigcomma_Nil_L)
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Bigcomma_Cons_L)
  apply (rule_tac rel=rel and beta="(''father'' @ `Suc n`)" in Swapout_R_1)
  using rel_refl apply (simp, simp)

  apply (rule_tac derivable.Back_forw_K2)
  apply (rule_tac f = "(One⇩F (''father'' @ `Suc n`)) →⇩F (`j` ⇩F)" in derivable.SingleCut)
  using cut apply simp

  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac f="(father (Suc n))" in derivable.Pre_L)
  using preFather unfolding preFormula_father_def apply blast

  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac f = "One⇩F (''father'' @ `Suc n`)" in derivable.SingleCut)
  using cut apply simp
  apply (rule_tac derivable.One_R)

  apply (rule_tac f="father (Suc n)" in derivable.Pre_L)
  using preFather unfolding preFormula_father_def apply blast
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply simp
  apply (rule_tac derivable.Reduce_R)
  apply (rule_tac derivable.ImpR_L)
  
  apply (rule_tac derivable.Atom)
  apply simp
  
  by (rule_tac derivable.One_R)
  (* end proof red_ax_1.cs *)

  have fboxK_map_subst: "⋀list. map (λh. fboxK⇩F `j` ((`h` ⇩F) →⇩F (`j` ⇩F))) list =  map (Formula_FboxK `j`)  (map (λh. ((`h` ⇩F) →⇩F (`j` ⇩F))) list)" by simp
  have map_subst: "map (λh. (`h` ⇩F) →⇩F (`j` ⇩F)) ( [[1 .. Suc n]]) = map (λB. B →⇩F (`j` ⇩F)) (map (Formula_Atprop ∘ nat_to_string) ( [[1 .. Suc n]]))" by simp
  have map_subst1: "set ( [[1 .. Suc n]]) = set ([h← [[1 .. Suc n]] .  h ≠ j]) ∪ {j}" 
  by (metis "0.prems"(1) "0.prems"(2) J_contains One_nat_def Un_insert_right `{1..Suc n} - {j} = set [x← [[1 .. Suc n]] . x ≠ j]` insert_Diff insert_subset sup_bot.right_neutral upto'_simp1)

  then have map_subst2: "set [[1 .. Suc n]] = set (j#[h← [[1 .. Suc n]] .  h ≠ j])" by simp

  have der1: "loc ⊢d (⋀⇩F map (λh. fboxK⇩F `j` ((`h` ⇩F) →⇩F (`j` ⇩F))) [h←[[1 .. Suc n]] . h ≠ j]) ⇩S ⊢⇩S 
    forwK⇩S `j` (father (Suc n) ⇩S) →⇩S ((`j` ⇩F) ⇩S)"
  apply (rule_tac f = "fboxK⇩F `j` (⋀⇩F map (λh. ((`h` ⇩F) →⇩F (`j` ⇩F))) [h ←  [[1 .. Suc n]]. h≠j])" in derivable.SingleCut)
  using cut apply simp
  apply(subst fboxK_map_subst)
  apply(rule_tac conj_box_distrib)
  using cut apply blast
  apply (rule_tac derivable.FboxK_L)
  unfolding father_def
  apply (rule_tac f = "(⋀⇩F map (λh. (`h` ⇩F) →⇩F (`j` ⇩F)) ( [[1 .. Suc n]]))" in derivable.SingleCut)
  using cut apply simp
  
  
  apply(rule_tac l="map (λh. (`h` ⇩F) →⇩F (`j` ⇩F)) (j#[h← [[1 .. Suc n]] .  h ≠ j])" in conj_der2b)
  using cut apply simp
  apply(subst conj_unfold_1a)
  
  apply (rule_tac derivable.I_impR2)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.And_R)
  apply (rule Id)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.W_impR_R)
  apply (rule_tac derivable.Id)
  using map_subst2 apply (metis (mono_tags, lifting) set_eq_subset set_map)

  apply(subst map_subst)
  apply(rule_tac disj_lub)
  using cut by simp


  have map_subst3: "∀h ∈ {1..Suc n} - {j}.
    loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S) ⊢⇩S 
    ((fboxK⇩F `j` ((`h` ⇩F) →⇩F (`j` ⇩F)))  ⇩S) ⟹
    loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S) ⊢⇩S 
    (⋀⇩F map (λh. fboxK⇩F `j` ((`h` ⇩F) →⇩F (`j` ⇩F))) [h←[[1 .. Suc n]] . h ≠ j]) ⇩S"
  apply(rule_tac conj_der1b)
  proof -
    assume a1: "∀h∈{1..Suc n} - {j}. loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S) ⊢⇩S fboxK⇩F `j` ((`h` ⇩F) →⇩F (`j` ⇩F)) ⇩S"
    { fix ff :: Formula
      have "ff ∈ (λn. fboxK⇩F `j` ((`n` ⇩F) →⇩F (`j` ⇩F))) ` ({1..Suc n} - {j}) ⟶ ff ∉ set (map (λn. fboxK⇩F `j` ((`n` ⇩F) →⇩F (`j` ⇩F))) [n←[[1 .. Suc n]] . n ≠ j]) ∨ loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S) ⊢⇩S ff ⇩S"
        using a1 by blast
      hence "ff ∉ set (map (λn. fboxK⇩F `j` ((`n` ⇩F) →⇩F (`j` ⇩F))) [n←[[1 .. Suc n]] . n ≠ j]) ∨ loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S) ⊢⇩S ff ⇩S"
        by (metis (no_types) set_eq set_map) }
    thus "∀f∈set (map (λn. fboxK⇩F `j` ((`n` ⇩F) →⇩F (`j` ⇩F))) [n←[[1 .. Suc n]] . n ≠ j]). loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S) ⊢⇩S f ⇩S"
      by blast
  qed


  have der2: "⋀h. h ∈ {1..Suc n} - {j} ⟹ loc ⊢d fdiamK⇩F `j` (((`h` ⇩F) →⇩F ⊥⇩F) ∧⇩F (`h` ⇩F)) ⇩S ⊢⇩S forwK⇩S `j` `j` ⇩F ⇩S"
  apply (rule_tac derivable.FdiamK_L)
  apply (rule_tac derivable.Forw_back_K2)
  apply (rule_tac f="⊥⇩F" in derivable.SingleCut)
  using cut apply blast
  apply (rule_tac derivable.Bot_R)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac derivable.Bot_L)
  apply (rule_tac derivable.Id)
  apply (rule_tac derivable.IW_R)
  by (rule_tac derivable.Bot_L)

  

  
  have fact_23_E_vision_der_vision: "(⋀h. h ∈ {1..Suc n} - {j} ⟹ 
    loc ⊢d (dirty (Suc n) J ⇩S) ;⇩S (vision (Suc n) ⇩S) ⊢⇩S (fboxK⇩F `j` ((`h` ⇩F) →⇩F ⊥⇩F)) ⇩S) ⟹ 
    (⋀h. h ∈ {1..Suc n} - {j} ⟹
    loc ⊢d (forwK⇩S `j` `h` ⇩F ⇩S) ;⇩S ((dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc 0 vision (Suc n) ⇩S) ;⇩S (father (Suc n) ⇩S)) ⊢⇩S 
    fdiamK⇩F `j` (((`h` ⇩F) →⇩F ⊥⇩F) ∧⇩F (`h` ⇩F)) ⇩S)"
  proof -
  case goal1 
    thus ?case
    apply (rule_tac f="(fboxK⇩F `j` ((`h` ⇩F) →⇩F ⊥⇩F)) ∧⇩F (fdiamK⇩F `j` (`h` ⇩F))" in derivable.SingleCut)
    using cut apply blast
    defer
    
    apply (rule_tac derivable.And_L)
    apply (rule_tac derivable.Comma_impR_disp2)
    apply (rule_tac derivable.FdiamK_L)
    apply (rule_tac derivable.Forw_back_K2)
    apply (rule_tac derivable.K_FS_R)
    apply (rule_tac derivable.Comma_impR_disp)
    apply (rule_tac derivable.Comma_impL_disp2)
    apply (rule_tac derivable.Back_forw_K)
    apply (rule_tac derivable.FboxK_L)
    apply (rule_tac derivable.Comma_impL_disp)
    apply (rule_tac derivable.Forw_back_K)
    apply (rule_tac derivable.FdiamK_R)
    apply (rule_tac derivable.And_R)
    apply (rule_tac Id)
    
    apply (rule_tac Id)
    
    apply (rule_tac derivable.E_L)
    
    apply (rule_tac derivable.And_R)
    apply (rule_tac derivable.FdiamK_R)
    apply (rule_tac Id)
    
    apply (rule_tac derivable.Comma_impR_disp2)
    apply (rule_tac derivable.W_impR_R)
    
    
    apply (rule_tac derivable.And_L)
    apply (rule_tac derivable.Comma_impR_disp2)
    apply (rule_tac f="vision (Suc n)" in derivable.SingleCut)
    using cut apply blast
    apply(rule E_der_simp2)
    using agent apply simp
    apply (rule_tac derivable.Comma_impR_disp)
    by simp
  qed



  
  have list_eq: "[x← [[1 .. Suc n]] . x ∉ set J] = [x← [[1 .. Suc n]] . x ≠ j]" using J_contains by simp
  with 0 have j_range: "0 < j ∧ j ≤ Suc n" by (simp add: J_contains)
  
  have f_subst: "((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) = ((λx. (`x` ⇩F) →⇩F ⊥⇩F))" by auto
  
  def left ≡ "(λx. ((`x` ⇩F) →⇩F fboxK⇩F `j` `x` ⇩F))"
  def right ≡ "(λy. (((`y` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`y` ⇩F) →⇩F ⊥⇩F))"
    

  have der3: "⋀h. h ∈ {1..Suc n} - {j} ⟹ loc ⊢d (dirty (Suc n) J ⇩S) ;⇩S (vision (Suc n) ⇩S) ⊢⇩S fboxK⇩F `j` ((`h` ⇩F) →⇩F ⊥⇩F) ⇩S"
  apply (rule_tac f="⋀⇩F map (λh. fboxK⇩F `j` ((`h` ⇩F) →⇩F ⊥⇩F)) [h← [[1 .. (Suc n)]] .  h ≠ j]" in derivable.SingleCut)
  using cut apply blast
  defer
  apply(rule_tac f="fboxK⇩F `j` ((`h` ⇩F) →⇩F ⊥⇩F)" in conj_der1)
  apply(rule Id)
  using set_eq apply fastforce
  apply (rule_tac derivable.Comma_impR_disp2)
  unfolding vision_def
  
  apply(rule_tac l'="map (λx. (left x) ∧⇩F (right x) ) [h← [[1 .. (Suc n)]] . h ≠ j]" in conj_der2)
  using cut apply simp
  
  apply(rule_tac f="(⋀⇩F map left [h← [[1 .. (Suc n)]] . h ≠ j]) ∧⇩F (⋀⇩F map right [h← [[1 .. (Suc n)]] . h ≠ j])" in SingleCut)
  using cut apply simp
  
  apply(rule_tac conj_fold)
  using cut apply simp
  unfolding right_def
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  unfolding dirty_def
  apply(rule_tac f="⋀⇩F map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. (Suc n)]] . x ≠ j]" in SingleCut)
  using cut apply simp
  apply(subst list_eq)
  
  apply(rule_tac l="map (Formula_Atprop ∘ nat_to_string) J @ map ((λx. (x ⇩F) →⇩F ⊥⇩F) ∘ nat_to_string) [x← [[1 .. (Suc n)]] . x ≠ j]" in conj_der2b)
  using cut apply simp
  using j_range J_contains using Id apply auto[1]
  apply simp
  apply (rule_tac derivable.Comma_impR_disp)
  
  apply(subst f_subst)
  
  apply (rule_tac E_L)
  apply (simp add: conj_impl_fold cut)
  proof -
  case goal1
    have "set [h← [[1 .. Suc n]] . h ≠ j] = { h. 0 < h ∧ h ≤ Suc n ∧ h≠j }" by auto
    
    then have a: "set (map (λh. ((`h` ⇩F) →⇩F fboxK⇩F `j` `h` ⇩F) ∧⇩F 
      (((`h` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`h` ⇩F) →⇩F ⊥⇩F)) [h← [[1 .. (Suc n)]] . h ≠ j]) =
      image (λh. ((`h` ⇩F) →⇩F fboxK⇩F `j` `h` ⇩F) ∧⇩F 
      (((`h` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`h` ⇩F) →⇩F ⊥⇩F)) { h. 0 < h ∧ h ≤ Suc n ∧ h≠j }" by simp
    then have b: "… = { (((`h`) ⇩F) →⇩F fboxK⇩F `j` (`h`) ⇩F) ∧⇩F 
      (((`h` ⇩F) →⇩F ⊥⇩F) →⇩F fboxK⇩F `j` (`h` ⇩F) →⇩F ⊥⇩F) | h. 0 < h ∧ h ≤ Suc n ∧ h≠j }" by blast
    
    then have "… ⊆ set (vision' (Suc n))" using vision_contains j_range by blast
    with a b show ?case by (simp add: left_def)
  qed

  show ?case
  apply (rule_tac red_ax_1)
  
  (* By DDT *)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.E_L)
  
  (*der 2*)
  apply (rule_tac f = "⋀⇩F map (λh. fboxK⇩F `j` ((`h` ⇩F) →⇩F (`j` ⇩F))) [h ←  [[1 .. Suc n]]. h≠j]" in derivable.SingleCut)
  using cut apply simp
  defer
  apply (rule der1)

  apply(rule_tac map_subst3)

  (* by FS2 *)
  apply rule
  apply(rule_tac FboxK_R)
  apply(rule_tac Back_forw_K2)
  apply(rule_tac ImpR_R)
  apply(rule_tac Back_forw_K)
  apply(rule_tac FS_K_R)
  (*By DDT 2*)
  apply (rule_tac derivable.Comma_impR_disp)

  (* mon_diamK_j *)
  apply (rule_tac f="fdiamK⇩F `j` (((`h` ⇩F) →⇩F ⊥⇩F) ∧⇩F (`h` ⇩F))" in derivable.SingleCut)
  using cut apply blast
  defer
  apply (rule der2)
  apply simp
  
  apply (rule fact_23_E_vision_der_vision)
  apply (rule der3)
  by simp

next
(* -------------------- successor case for k  --------------------  *)
case (Suc k) (* the number of dirty children is Suc(Suc k) *)

  then obtain J' where J'_def: "set J' = set J - {j}" by (meson set_removeAll)
  then obtain j' where j'_def: "j' ∈ set J'" by (metis Diff_empty List.finite_set Suc(4) Suc.prems(4) card_Diff_insert card_eq_SucD diff_Suc_1 empty_iff insert_subset order_refl)
  
  with Suc J'_def have "card (set J') = Suc k" by simp
  with Suc have ih: " ∀j∈set J'. loc ⊢d (dirty (Suc n) J' ∧⇩F E (Suc n) ⇧Suc k vision (Suc n) )⇩S ⊢⇩S 
    (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j` (`j` ⇩F)) ⇩S" using Diff_subset Suc_leD J'_def subsetCE subsetI
  proof -
    have "set J' ⊆ {1..Suc n}"
      by (metis (no_types) Diff_subset Suc.prems(2) J'_def subsetCE subsetI)
    thus ?thesis
      by (meson Suc.hyps Suc.prems(1) Suc_leD `card (set J') = Suc k`)
  qed


(* ------------------ start of claim 1 ------------------ *)

  have claim10: "loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc (Suc k) vision (Suc n)) ⇩S ⊢⇩S 
  (dirty (Suc n) J ∧⇩F ( vision (Suc n) ∧⇩F fboxK⇩F `j` ( E (Suc n) ⇧Suc k vision (Suc n))))⇩S"
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.And_R)
  defer
  apply(rule Id)
  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.And_R)
  apply(subst k_apply.simps)
  apply (rule E_der_simp)
  using Suc j'_def apply auto[1]
  apply(rule E_der_simp2)
  using assms by simp



  have claim11:  "loc ⊢d (dirty (Suc n) J ∧⇩F ( vision (Suc n) ∧⇩F fboxK⇩F `j` ( E (Suc n) ⇧Suc k vision (Suc n))))⇩S ⊢⇩S 
  ( (fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' )) ∧⇩F (fboxK⇩F `j` ( E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S"

  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.A_L)
  apply (rule_tac derivable.And_R)
  apply (rule_tac Id)
  
  apply(rule_tac dirty_vision_der)
  using Suc(2,3,5) J'_def cut by auto

  have claim12: "loc ⊢d ( (fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' )) ∧⇩F (fboxK⇩F `j` ( E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S ⊢⇩S 
  ( fboxK⇩F `j` (( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' ) ∧⇩F ( E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S"
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Back_forw_K2)
  apply (rule_tac derivable.K_mon_L)
  apply (rule_tac derivable.And_R)
  
  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac Id)
  
  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac Id)
  by (rule_tac Id)

  have claim13: "loc ⊢d ( fboxK⇩F `j` (( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' ) ∧⇩F ( E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S ⊢⇩S 
  ( fboxK⇩F `j` (( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' ) ∧⇩F ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S"

  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.And_R)
  
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply (rule_tac Id)
  
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac Id)
  by (rule_tac Id)
  
  have claim14: "loc ⊢d ( fboxK⇩F `j` (( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' ) ∧⇩F ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S ⊢⇩S 
  ( fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( dirty (Suc n) J' ∧⇩F E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S"
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.A_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.A_L2)
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.A_L)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.And_R)
  
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac Id)
  apply (rule_tac Id)
  
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac Id)
  by (rule_tac Id)
  

  
  have claim15: "loc ⊢d ( fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( dirty (Suc n) J' ∧⇩F E (Suc n) ⇧Suc k vision (Suc n) )) )⇩S ⊢⇩S 
  ( fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) )) )⇩S"
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  defer
  apply (rule Id)
  using ih Id j'_def by simp
  
  
  have claim16: "loc ⊢d ( fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) )) )⇩S ⊢⇩S 
  ( fboxK⇩F `j` ( (((`j` ⇩F) →⇩F ⊥⇩F ) ∧⇩F father (Suc n) ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) )) )⇩S"
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac Id)
  
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.W_impR_R)
  by (rule_tac Id)


  have claim1: "loc ⊢d (dirty (Suc n) J ∧⇩F E (Suc n) ⇧Suc (Suc k) vision (Suc n)) ⇩S ⊢⇩S 
   ( fboxK⇩F `j` ( (((`j` ⇩F) →⇩F ⊥⇩F ) ∧⇩F father (Suc n) ) →⇩F ( (fboxA⇩F (''father'' @
       `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) )) )⇩S"
  apply (rule_tac f="dirty (Suc n) J ∧⇩F (vision (Suc n) ∧⇩F fboxK⇩F `j` E (Suc n) ⇧Suc k vision (Suc n))" in derivable.SingleCut)
  using cut apply simp
  using claim10 apply simp
  
  apply (rule_tac f="fboxK⇩F `j` ((`j` ⇩F) →⇩F ⊥⇩F) →⇩F dirty (Suc n) J' ∧⇩F
    fboxK⇩F `j` E (Suc n) ⇧Suc k vision (Suc n)" in derivable.SingleCut)
  using cut apply simp
  using claim11 apply simp
  
  apply (rule_tac f="fboxK⇩F `j` (( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' ) ∧⇩F ( E (Suc n) ⇧Suc k vision (Suc n) ))" in derivable.SingleCut)
  using cut apply simp
  using claim12 apply simp
  
  apply (rule_tac f=" fboxK⇩F `j` (( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F dirty (Suc n) J' ) ∧⇩F ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F E (Suc n) ⇧Suc k vision (Suc n) ))" in derivable.SingleCut)
  using cut apply simp
  using claim13 apply simp
  
  apply (rule_tac f="fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( dirty (Suc n) J' ∧⇩F E (Suc n) ⇧Suc k vision (Suc n) ))" in derivable.SingleCut)
  using cut apply simp
  using claim14 apply simp
  
  apply (rule_tac f="fboxK⇩F `j` ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
       `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ))" in derivable.SingleCut)
  using cut apply simp
  using claim15 apply simp
  
  apply (rule_tac f="fboxK⇩F `j` ( (((`j` ⇩F) →⇩F ⊥⇩F ) ∧⇩F father (Suc n) ) →⇩F ( (fboxA⇩F (''father'' @
       `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ))" in derivable.SingleCut)
  using cut apply simp
  using claim16 apply simp
  
  by (rule_tac Id)

(* ------------------- end of claim 1 ------------------- *)

(* ------------------ start of claim 2 ------------------ *)


(* In lem363_ we prove the different steps of Lemma 36.3 -- see p23 of the paper Ma Pal Sad*) 
    
  have lem363a: "loc ⊢d ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ))) ∧⇩F 
   (fdiamA⇩F (''father'' @
   `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k (no (Suc n) )) )⇩S
   ⊢⇩S ( ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ) ) )∧⇩F (
   ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F
   (fdiamA⇩F (''father'' @
   `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k(no (Suc n) )) ) )
   )⇩S" 
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.And_R)
  
  defer
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  apply (rule Id)
  
  apply (rule Id)
  
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply (rule Id)
  done
  
  
  have lem363b: "loc ⊢d
   ( ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ) ) )∧⇩F (
   ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F
   (fdiamA⇩F (''father'' @
   `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k (no (Suc n) )) ) )
   )⇩S
   ⊢⇩S 
   ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( (fboxA⇩F (''father'' @
   `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ) ∧⇩F 
   (fdiamA⇩F (''father'' @
   `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k(no (Suc n) )) )
  ) )⇩S" 
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.C_L)
  apply (rule_tac derivable.Comma_impL_disp)
  apply (rule_tac derivable.A_L2)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.A_L2)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.A_L)
  apply (rule_tac derivable.And_R)
  
  defer
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule Id)
  apply (rule Id)
  
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule Id)
  apply (rule Id)
  done

  have lem363c: "loc ⊢d
  ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( 
    (fboxA⇩F (''father'' @ `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ) ∧⇩F 
    (fdiamA⇩F (''father'' @ `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k(no (Suc n))) )
  ) )⇩S ⊢⇩S 
  ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( 
    (fboxA⇩F (''father'' @ `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ) ∧⇩F 
    (fdiamA⇩F (''father'' @ `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) )
  ) )⇩S" 
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  defer
  apply (rule Id)
  
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.And_R)
  defer
  apply (rule Id)
  
  apply (rule_tac derivable.FdiamA_L)
  apply (rule_tac derivable.FdiamA_R)
  
  apply(subst k_apply_elim_diamA)
  defer apply(simp)
  apply (rule_tac f = "(fdiamK⇩F `j'` ( (`j'` ⇩F) )) ∧⇩F (fdiamK⇩F `j'` ( (`j'` ⇩F) →⇩F ⊥⇩F ))" in derivable.SingleCut)
  using cut apply simp
  defer
  
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impL_disp2)
  apply (rule_tac derivable.W_impL_L)
  apply (rule Id)
  apply(rule no_imp)

  using j'_def J'_def Suc(3) by force
  
  
  have lem363d: "loc ⊢d
   ( ( (fboxA⇩F (''father'' @
   `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ) ∧⇩F 
   (fdiamA⇩F (''father'' @
   `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) )
  ) )⇩S ⊢⇩S ( (fdiamA⇩F (''father'' @
   `Suc n`) ( ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) 
   ∧⇩F ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) )) )⇩S" 
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.FdiamA_L)
  apply (rule_tac derivable.Forw_back_A2)
  apply (rule_tac derivable.A_FS_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.Forw_back_A)
  apply (rule_tac derivable.FdiamA_R)
  apply (rule_tac derivable.And_R)
  defer
  apply (rule_tac derivable.Back_forw_A)
  apply (rule_tac derivable.FboxA_L)
  apply (rule Id)
  apply (rule Id)
  done
  
  
  have lem363e: "loc ⊢d
   ( ( ( ( Formula_FboxA (''no'' @ `Suc n`) ⇧k ( fboxK⇩F `j'` (`j'` ⇩F)) )) ∧⇩F 
   ( ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k (fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F))) )
  ) )⇩S ⊢⇩S ( ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k ( ( fboxK⇩F `j'` (`j'` ⇩F)) 
   ∧⇩F ( fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) )) )⇩S" 
  
  apply (subst k_apply_BoxDiam)
  using cut apply simp
  apply simp
  done
  
  have lem363f: "loc ⊢d
   ( ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k ( ( fboxK⇩F `j'` (`j'` ⇩F)) 
   ∧⇩F ( fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) )) )⇩S ⊢⇩S ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k ( ⊥⇩F )) ⇩S" 
  apply (rule k_apply_elim_diamA )
  apply (rule_tac derivable.Bot_R)
  apply (rule_tac a="`j'`" in derivable.Refl_ForwK)
  using agent apply simp
  apply (rule_tac derivable.And_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.FdiamK_L)
  apply (rule_tac derivable.Forw_back_K2)
  apply (rule_tac derivable.K_FS_R)
  apply (rule_tac derivable.ImpR_L)
  defer
  apply (rule_tac derivable.Back_forw_K)
  apply (rule_tac derivable.FboxK_L)
  apply (rule Id)
  apply (rule_tac derivable.IW_R)
  apply (rule_tac derivable.Bot_L) 
  done
  
  have lem363: "loc ⊢d ( ((`j` ⇩F) →⇩F ⊥⇩F ) →⇩F ( 
    (fboxA⇩F (''father'' @  `Suc n`) ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ))) ∧⇩F 
    (fdiamA⇩F (''father'' @ `Suc n`) ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k (no (Suc n) )) )⇩S
  ⊢⇩S ( ((`j` ⇩F)→⇩F ⊥⇩F)→⇩F ⊥⇩F )⇩S" 
  apply(rule_tac f=" (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F
    fboxA⇩F (''father'' @  `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` `j'` ⇩F) ∧⇩F
    (((`j` ⇩F) →⇩F ⊥⇩F) →⇩F
        fdiamA⇩F (''father'' @ `Suc n`) Formula_FdiamA (''no'' @ `Suc n`) ⇧k no (Suc n))" in derivable.SingleCut)
  using cut apply simp
  using lem363a apply simp
  
  
  apply (rule_tac f="((`j` ⇩F) →⇩F ⊥⇩F) →⇩F
    ( (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` )⇩F ) ∧⇩F
    ( fdiamA⇩F (''father'' @ `Suc n`) Formula_FdiamA (''no'' @ `Suc n`) ⇧k no (Suc n)))" in derivable.SingleCut)
  using cut apply simp
  using lem363b apply simp
  
  apply (rule_tac f=" ((`j` ⇩F) →⇩F ⊥⇩F) →⇩F
   ( (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` `j'` ⇩F ) ∧⇩F
   ( fdiamA⇩F (''father'' @ `Suc n`) Formula_FdiamA (''no'' @ `Suc n`) ⇧k fdiamK⇩F `j'` ( (`j'` ⇩F) →⇩F ⊥⇩F) )) " in derivable.SingleCut)
  using cut apply simp
  using lem363c apply simp
  
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_L)
  defer
  apply (rule Id)
  
  apply (rule_tac f="(fdiamA⇩F (''father'' @ `Suc n`) ( ( Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ∧⇩F
    ( Formula_FdiamA (''no'' @ `Suc n`) ⇧k fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) ))" in derivable.SingleCut)
  using cut apply simp

  using lem363d apply simp
  
  apply (rule_tac derivable.FdiamA_L)
  apply (rule_tac derivable.Forw_back_A2)
  
      
  apply (rule_tac f="( Formula_FdiamA (''no'' @ `Suc n`) ⇧k ( ( fboxK⇩F `j'` (`j'` ⇩F)) ∧⇩F
    ( fdiamK⇩F `j'` ((`j'` ⇩F)→⇩F ⊥⇩F)) ))" in derivable.SingleCut)
  using cut apply simp
  using lem363e apply simp
      
  apply (rule_tac f="Formula_FdiamA (''no'' @ `Suc n`) ⇧k ⊥⇩F" in derivable.SingleCut)
  using cut apply simp
  using lem363f apply simp

  
  apply (rule_tac derivable.Forw_back_A)
  apply (rule_tac derivable.Bot_R)
  apply (rule_tac derivable.Forw_back_A2)
  apply (rule_tac derivable.A_nec_R)
  by (rule_tac k_apply_DiamBot)
   
  
  have claim2: "loc ⊢d ( fboxK⇩F `j` ( (((`j` ⇩F) →⇩F ⊥⇩F ) ∧⇩F father (Suc n) ) →⇩F ( 
    (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) )) )⇩S ⊢⇩S 
    (fboxK⇩F `j` (( father (Suc n) ) →⇩F ( (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k (`j` ⇩F)) )) )⇩S"
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac f = "(father (Suc n)) →⇩F ((((`j` ⇩F) →⇩F ⊥⇩F ) ) →⇩F ( 
    (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ))" in derivable.SingleCut)
  using cut apply simp
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.A_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule Id)
  apply (rule_tac derivable.And_R)
  apply (rule Id)
  apply (rule Id)
  
  apply (rule_tac derivable.ImpR_L)
  defer
  apply (rule_tac Id)
  
  apply (rule_tac derivable.FboxA_R)
  apply (rule_tac derivable.Back_forw_A2)
  
  
  apply(subst k_apply_unfold_bis)
  apply(subst k_apply_S_display_1)
  using cut apply simp
  apply(subst k_apply_S_display_2)
  
  apply (rule_tac derivable.FboxA_R)
  apply (rule_tac f="(One⇩F ((''no'' @ `Suc n`))) →⇩F ( `j` ⇩F) " in derivable.SingleCut)
  using cut apply simp
  defer
  
  apply (rule_tac derivable.Reduce_R)
  apply (rule_tac derivable.ImpR_L)
  defer
  apply (rule_tac derivable.One_R)
  defer
  apply (rule_tac derivable.Atom)
  apply (simp)
  


  apply (rule_tac derivable.ImpR_R)
  apply(subst k_apply_S_display_2back)

  apply (rule_tac k_apply_S_FS)


  apply (rule_tac derivable.Back_forw_A)
  apply (rule_tac derivable.FS_A_R)
  apply (rule_tac derivable.Comma_impR_disp)

  apply (rule_tac derivable.E_L)
  
  
  apply (rule_tac f= "(((`j` ⇩F) →⇩F ⊥⇩F) →⇩F fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` `j'` ⇩F) ∧⇩F
    fdiamA⇩F (''father'' @ `Suc n`) Formula_FdiamA (''no'' @ `Suc n`) ⇧k no (Suc n)" in derivable.SingleCut)
  using cut apply blast
  apply (rule_tac derivable.And_R)
  apply (rule_tac derivable.FdiamA_R)

  apply (rule_tac k_apply_S_F_forw_diam)
  apply (rule_tac f="no (Suc n)" in derivable.Pre_L)
  using preNo unfolding preFormula_no_def apply blast
  apply(rule Id)+
  
  apply(rule_tac f = "((`j` ⇩F) →⇩F ⊥⇩F) →⇩F ⊥⇩F" in derivable.SingleCut)
  using cut apply simp
  using lem363 apply simp
  apply (rule_tac f="`j` ⇩F" in derivable.SingleCut)
  using cut apply blast
  defer
  apply (rule k_apply_S_Atom)
  using cut apply simp
  apply (rule_tac derivable.C_R)
  apply (rule_tac derivable.I_impR2)
  apply (rule_tac derivable.Grishin_R2)
  apply (rule_tac derivable.E_R)
  apply (rule_tac derivable.ImpR_comma_disp2)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.E_L)
  apply (rule_tac derivable.Comma_impR_disp2)
  apply (rule_tac derivable.ImpR_L)
  apply (rule_tac derivable.IW_R)
  apply (rule_tac derivable.Bot_L)

  apply (rule_tac derivable.ImpR_R)
  apply (rule_tac derivable.ImpR_comma_disp)
  apply (rule_tac derivable.E_R)
  apply (rule_tac derivable.Grishin_R)
  apply (rule_tac derivable.W_impR_R)
  apply (rule_tac derivable.ImpL_comma_disp2)
  apply (rule_tac derivable.W_impL_R)
  apply (rule_tac derivable.Id)
  done

(* ------------------- end of claim 2 ------------------- *)

(* ------------------ start of claim 3 ------------------ *)

  have claim3: "loc ⊢d ( fboxK⇩F `j` (( father (Suc n) ) →⇩F ( 
    (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k (`j` ⇩F)) )) )⇩S ⊢⇩S 
    ( (fboxA⇩F (''father'' @  `Suc n`) fboxK⇩F `j` ( Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k (`j` ⇩F)) ) )⇩S"
  apply (rule_tac derivable.FboxA_R)
  apply (rule_tac derivable.Back_forw_A2)
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac derivable.Back_forw_A)
  apply (rule_tac derivable.I_impR2)
  apply (rule_tac derivable.Bigcomma_Nil_L)
  apply (rule_tac derivable.Comma_impR_disp)
  apply (rule_tac derivable.Bigcomma_Cons_L)
  apply(rule_tac rel=rel and beta="''father'' @ `Suc n`" in Swapout_R_1)
  using rel_refl apply (simp,simp)
  
  
  apply (rule_tac derivable.FboxK_L)
  apply (rule_tac derivable.Reduce_R)
  apply (rule_tac derivable.ImpR_L)
  
  apply (rule_tac derivable.FboxA_L)
  apply (rule_tac Id)
  apply (rule_tac f="One⇩F (''father'' @ `Suc n`)" in derivable.SingleCut)
  using cut apply simp
  apply (rule_tac derivable.One_R)
  
  apply (rule_tac f="father (Suc n)" in derivable.Pre_L)
  using preFather unfolding preFormula_father_def apply blast
  by (rule_tac Id)

(* ------------------- end of claim 3 ------------------- *)

(* ------------------ start of claim 4 ------------------ *)

  have claim4: "loc ⊢d 
    ( (fboxA⇩F (''father'' @ `Suc n`)  fboxK⇩F `j` (  Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k (`j` ⇩F)) ) )⇩S ⊢⇩S 
    (fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k fboxK⇩F `j` `j` ⇩F) ⇩S"
  apply (rule_tac derivable.FboxA_R)
  apply (rule_tac derivable.FboxA_L)
  
  apply (subst k_apply_S_display_1)
  using cut apply simp
  apply (subst k_apply_S_display_2)
  apply (rule_tac derivable.FboxK_R)
  apply (rule_tac k_apply_S_display_2a)
  apply (rule_tac rel=rel in Swapout_R_2)
  using cut rel_refl by simp+
  
(* ------------------- end of claim 4 ------------------- *)

  show ?case
  apply (rule_tac f="fboxK⇩F `j` ( (((`j` ⇩F) →⇩F ⊥⇩F ) ∧⇩F father (Suc n) ) →⇩F ( (fboxA⇩F (''father'' @
    `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧k fboxK⇩F `j'` (`j'` ⇩F)) ))" in derivable.SingleCut)
  using cut apply simp
  using claim1 Suc apply blast

  apply (rule_tac f="fboxK⇩F `j` (( father (Suc n) ) →⇩F ( (fboxA⇩F (''father'' @
    `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k (`j` ⇩F)) ))" in derivable.SingleCut)
  using cut apply simp
  using claim2 Suc apply blast

  apply (rule_tac f="(fboxA⇩F (''father'' @
    `Suc n`)  fboxK⇩F `j` ( (Formula_FboxA (''no'' @ `Suc n`)) ⇧Suc k (`j` ⇩F)) )" in derivable.SingleCut)
  using cut apply simp
  using claim3 apply simp

  apply (rule_tac f="fboxA⇩F (''father'' @ `Suc n`) Formula_FboxA (''no'' @ `Suc n`) ⇧Suc k fboxK⇩F `j` `j` ⇩F" in derivable.SingleCut)
  using cut apply simp
  using claim4 apply simp
  using Id by blast
qed
end