Theory KoenigLemma

(*  Formalization of König Lemma
   Fabian Fernando Serrano Suárez  UNAL Manizales
   Thaynara Arielly de Lima        Universidade Federal de Goiáis 
   Mauricio Ayala-Rincón           Universidade de Brasília
*)

(*<*)
theory KoenigLemma
 imports PropCompactness  
begin
(*>*)

section ‹König Lemma›

text‹This section formalizes König Lemma from the compactness theorem for propositional logic directly. ›


type_synonym 'a rel = "('a × 'a) set"

definition irreflexive_on ::  "'a set ⇒ 'a rel ⇒ bool"
 where "irreflexive_on A r ≡  (∀x∈A. (x, x) ∉ r)"

definition transitive_on :: "'a set ⇒ 'a rel ⇒ bool"
  where "transitive_on A r ≡
 (∀x∈A. ∀y∈A. ∀z∈A. (x, y) ∈ r ∧ (y, z) ∈ r ⟶ (x, z) ∈ r)"

definition total_on :: "'a set ⇒ 'a rel ⇒ bool"
  where "total_on A r ≡ (∀x∈A. ∀y∈A. x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r)"

definition minimum ::  "'a set ⇒ 'a ⇒'a rel ⇒ bool"
  where "minimum A a r ≡  (a∈A ∧ (∀x∈A. x ≠ a  ⟶ (a,x) ∈ r))"

definition predecessors :: "'a set ⇒'a ⇒'a rel  ⇒ 'a set"
  where "predecessors A a r ≡ {x∈A.(x, a) ∈ r}"

definition height ::  "'a set ⇒'a ⇒ 'a rel ⇒ nat"
  where "height A a r   ≡  card (predecessors A a r)"

definition level ::  "'a set ⇒ 'a rel ⇒ nat ⇒'a set"
  where "level A r n ≡ {x∈A. height A x r = n}"

definition imm_successors ::  "'a set ⇒ 'a ⇒ 'a rel ⇒ 'a set"
  where "imm_successors A a r ≡ 
 {x∈A. (a,x)∈ r ∧ height A x r = (height A a r)+1}" 

definition strict_part_order ::  "'a set ⇒ 'a rel ⇒ bool"
  where  "strict_part_order A r ≡ irreflexive_on A r ∧ transitive_on A r"

lemma minimum_element:
  assumes  "strict_part_order A r" and "minimum A a r" and "r={}"
  shows "A={a}"
proof(rule ccontr)
  assume hip: "A ≠ {a}" show False
  proof(cases)
    assume  hip1: "A={}"
    have "a∈A" using `minimum A a r` by(unfold minimum_def, auto) 
    thus False using hip1 by auto
  next
    assume  "A ≠ {}"
    hence "∃x. x≠a ∧ x∈A" using hip by auto
    then obtain x where  "x≠a ∧ x∈A" by auto
    hence "(a,x)∈r"  using `minimum A a r` by(unfold minimum_def, auto)
    hence "r ≠ {}" by auto
    thus False using `r={}` by auto
  qed
qed

lemma spo_uniqueness_min:
  assumes  "strict_part_order A r" and  "minimum A a r" and "minimum A b r" 
  shows "a=b"
proof(rule ccontr)
  assume hip: "a ≠ b"
  have "a∈A"and "b∈A" using assms(2-3) by(unfold minimum_def, auto)
  show False
  proof(cases)
    assume "r = {}"
    hence  "A={a} ∧ A={b}"  using assms(1-3) minimum_element[of A r] by auto
    thus False using hip by auto
  next
    assume "r≠{}"
    hence 1: "(a,b)∈r ∧ (b,a)∈r" using hip assms(2-3)
      by(unfold minimum_def, auto)    
    have  irr: "irreflexive_on A r" and tran: "transitive_on A r"     
    using assms(1) by(unfold strict_part_order_def, auto)
    have  "(a,a)∈r" using  `a∈A`  `b∈A` 1 tran by(unfold transitive_on_def, blast)
    thus False using  `a∈A`  irr  by(unfold irreflexive_on_def, blast)
  qed
qed

lemma emptyness_pred_min_spo:
  assumes  "minimum A a r" and "strict_part_order A r"
  shows  "predecessors A a r = {}"
proof(rule ccontr)
  have  irr:  "irreflexive_on A r" and tran: "transitive_on A r" using assms(2)
  by(unfold strict_part_order_def, auto)
  assume 1: "predecessors A a r ≠ {}" show False
  proof-
    have "∃x∈A. (x,a)∈ r" using 1  by(unfold predecessors_def, auto)
    then obtain x where "x∈A" and "(x,a)∈ r" by auto
    hence "x≠a" using irr by (unfold irreflexive_on_def, auto)
    hence "(a,x)∈r" using  `x∈A` `minimum A a r` by(unfold minimum_def, auto)
    have  "a∈A" using  `minimum A a r` by(unfold minimum_def, auto)
    hence "(a,a)∈r" using `(a,x)∈r`  `(x,a)∈ r`  `x∈A`  tran 
      by(unfold transitive_on_def, blast)
    thus False using `(a,a)∈r` `a∈A` irr  irreflexive_on_def
      by (unfold irreflexive_on_def, auto)
  qed
qed

lemma  emptyness_pred_min_spo2:
  assumes  "strict_part_order A r" and  "minimum A a r" 
  shows "∀x∈A.(predecessors A x r = {}) ⟷ (x=a)" 
proof
  fix x
  assume  "x ∈ A" 
  show "(predecessors A x r = {}) ⟷ (x = a)"
  proof-
    have 1: "a ∈ A" using  `minimum A a r`  by(unfold minimum_def, auto)
    have 2: "(predecessors A x r = {})⟶ (x=a)"
    proof(rule impI)
      assume h: "predecessors A x r = {}"  show "x=a"
      proof(rule ccontr)
      assume  "x ≠ a" 
      hence  "(a,x)∈ r" using  `x ∈ A` `minimum A a r`
        by(unfold minimum_def, auto)     
      hence  "a ∈ predecessors A x r"
        using 1 by(unfold  predecessors_def,auto)
      thus False using h by auto 
    qed
  qed
  have 3: "x=a ⟶ (predecessors A x r = {})"
  proof(rule impI)
    assume "x=a"
    thus "predecessors A x r = {}" 
      using assms emptyness_pred_min_spo[of A a]  by auto
  qed
  show ?thesis using 2 3 by auto
   qed
qed

lemma height_minimum:
  assumes  "strict_part_order A r" and  "minimum A a r"
  shows "height  A a r = 0"
proof-
  have  "a∈A" using  `minimum A a r` by(unfold minimum_def, auto)
  hence "predecessors A a r = {}"
    using assms emptyness_pred_min_spo2[of A r]  by auto
  thus "height  A a r = 0" by(unfold height_def, auto) 
qed

lemma zero_level:
  assumes  "strict_part_order A r" 
  and "minimum A a r"  and  "∀x∈A. finite (predecessors A x r)"  
  shows "(level A r 0) = {a}"
proof-
  have "∀x∈A.(card (predecessors A x r) = 0) ⟷ (x=a)"
  using  assms emptyness_pred_min_spo2[of A r a] card_eq_0_iff by auto
  hence 1:  "∀x∈A.(height A x r = 0) ⟷ (x=a)"
    by(unfold height_def, auto)
  have "a∈A" using  `minimum A a r` by(unfold minimum_def, auto)
  thus ?thesis using assms 1  level_def[of A r 0] by auto
qed

lemma min_predecessor:
  assumes  "minimum A a r"
  shows  "∀x∈A. x≠a ⟶ a∈predecessors A x r"
proof
  fix x
  assume "x∈A"
  show "x ≠ a ⟶ a ∈ predecessors A x r"
  proof(rule impI)
    assume  "x ≠ a"
    show "a ∈ predecessors A x r"
    proof-
      have "(a,x)∈r" using `x∈A` `x ≠ a` `minimum A a r` 
        by(unfold minimum_def, auto)
      hence "a∈A"  using  `minimum A a r` by(unfold minimum_def, auto)
      thus "a∈predecessors A x r" using `(a,x)∈r` 
        by(unfold predecessors_def, auto)
    qed
  qed
qed

lemma spo_subset_preservation: 
  assumes "strict_part_order A r" and "B⊆A" 
  shows "strict_part_order B r" 
proof-  
  have  "irreflexive_on A r" and "transitive_on A r" 
    using  `strict_part_order A r` 
    by(unfold strict_part_order_def, auto)
  have 1: "irreflexive_on B r"
  proof(unfold irreflexive_on_def)
    show "∀x∈B. (x, x) ∉ r"
    proof
      fix x
      assume "x∈B" 
      hence "x∈A" using  `B⊆A` by auto
      thus "(x,x)∉r" using  `irreflexive_on A r`
        by (unfold irreflexive_on_def, auto)
    qed
  qed
  have 2:  "transitive_on B r"
  proof(unfold transitive_on_def)
    show "∀x∈B. ∀y∈B. ∀z∈B. (x, y) ∈ r ∧ (y, z) ∈ r ⟶ (x, z) ∈ r"
    proof
      fix x assume "x∈B"
      show "∀y∈B. ∀z∈B. (x, y) ∈ r ∧ (y, z) ∈ r ⟶ (x, z) ∈ r"
      proof
        fix y  assume "y∈B"
        show "∀z∈B. (x, y) ∈ r ∧ (y, z) ∈ r ⟶ (x, z) ∈ r"
        proof 
          fix z  assume "z∈B"
          show "(x, y) ∈ r ∧ (y, z) ∈ r ⟶ (x, z) ∈ r"
          proof(rule impI)
            assume hip: "(x, y) ∈ r ∧ (y, z) ∈ r" 
            show "(x, z) ∈ r"
          proof-
            have "x∈A" and  "y∈A" and  "z∈A" using `x∈B` `y∈B` `z∈B` `B⊆A`
              by auto
            thus "(x, z) ∈ r" using hip `transitive_on A  r` by(unfold transitive_on_def, blast)
            qed
          qed
        qed
      qed
    qed
  qed
  thus "strict_part_order B r"
    using 1 2  by(unfold strict_part_order_def, auto)   
qed

lemma total_ord_subset_preservation:
  assumes "total_on A r" and  "B⊆A"
  shows "total_on B r"
proof(unfold total_on_def)
  show  "∀x∈B. ∀y∈B. x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r"
  proof
    fix x
    assume "x∈B" show " ∀y∈B. x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r"
    proof 
      fix y
      assume "y∈B" 
      show  "x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r"  
      proof(rule impI)
        assume  "x ≠ y"
        show "(x, y) ∈ r ∨ (y, x) ∈ r"
        proof-
          have "x∈A ∧ y∈A" using  `x∈B`  `y∈B` `B⊆A` by auto
          thus  "(x, y) ∈ r ∨ (y, x) ∈ r" 
            using  `x ≠ y` `total_on A r` by(unfold total_on_def, auto) 
        qed
      qed
    qed
  qed
qed

definition maximum ::  "'a set ⇒ 'a ⇒'a rel ⇒ bool"
  where "maximum A a r ≡  (a∈A ∧ (∀x∈A. x ≠ a ⟶ (x,a) ∈ r))"

lemma maximum_strict_part_order:
  assumes "strict_part_order A r" and "A≠{}" and "total_on A r" 
  and "finite A"
  shows "(∃a. maximum A a r)" 
proof-
  have "strict_part_order A r ⟹ A≠{} ⟹ total_on A r ⟹ finite A
  ⟹ (∃a. maximum A a r)"  using assms(4)
  proof(induct A rule:finite_induct)
    case empty
    then show ?case by auto
  next
    case (insert x A)  
    show "(∃a. maximum (insert x A) a r)"
  proof(cases "A={}")
    case True
    hence "insert x A ={x}" by simp
    hence  "maximum (insert x A) x r" by(unfold maximum_def, auto)
    then show ?thesis by auto
  next
    case False
    assume "A ≠ {}"
    show "∃a. maximum (insert x A) a r"
    proof-
      have 1: "strict_part_order A r" 
        using insert(4) spo_subset_preservation by auto
      have 2: "total_on A r" using insert(6) total_ord_subset_preservation by auto
      have "∃a. maximum A a r" using 1  `A≠{}`  insert(1) 2 insert(3) by auto
      then obtain a where a: "maximum A a r" by auto
      hence  "a∈A" and "∀y∈A. y ≠ a  ⟶ (y,a) ∈ r" by(unfold maximum_def, auto)
      have 3: "a∈(insert x A)" using `a∈A`  by auto
      have 4: "a≠x" using `a∈A` and  `x ∉ A` by auto
      have  "x∈(insert x A)" by auto
      hence "(a,x)∈r ∨ (x,a)∈r" using 3 4 `total_on (insert x A) r`
        by(unfold total_on_def, auto)
      thus "∃a. maximum (insert x A) a r"
      proof(rule disjE)
        have  "transitive_on (insert x A) r" using  insert(4) 
          by(unfold strict_part_order_def, auto) 
        assume casoa: "(a, x) ∈ r"  
        have  "∀z∈(insert x A). z ≠ x  ⟶ (z,x) ∈ r"
        proof
          fix z
          assume hip1: "z ∈ (insert x A)"
          show "z ≠ x ⟶ (z, x) ∈ r"
          proof(rule impI)
            assume "z ≠ x"
            hence hip2:  "z∈A" using `z ∈ (insert x A)` by auto 
            thus "(z, x) ∈ r" 
            proof(cases)
              assume "z=a" 
              thus "(z, x) ∈ r" using `(a, x) ∈ r` by auto 
            next
              assume "z≠a"
              hence "(z,a) ∈ r" using  `z∈A` `∀y∈A. y ≠ a  ⟶ (y,a) ∈ r` by auto
              have "a∈(insert x A)" and "z∈(insert x A)" and  "x∈(insert x A)"
                using  `a∈A` `z∈A` by auto            
              thus  "(z, x) ∈ r"
                using  `(z,a) ∈ r` `(a, x) ∈ r`  `transitive_on (insert x A) r`
                by(unfold transitive_on_def, blast) 
            qed
          qed
        qed
        thus "∃a. maximum (insert x A) a r"
          using  `x∈(insert x A)` by(unfold maximum_def, auto)
      next
        assume casob: "(x, a) ∈ r"
        have  "∀z∈(insert x A). z ≠ a  ⟶ (z,a) ∈ r"
        proof
          fix z
          assume hip1: "z ∈ (insert x A)"
          show "z ≠ a ⟶ (z, a) ∈ r"
          proof(rule impI)
            assume "z ≠ a" show  "(z, a) ∈ r"
            proof- 
              have "z∈A ∨ z=x" using `z ∈ (insert x A)` by auto
              thus  "(z, a) ∈ r"
              proof(rule disjE)
                assume  "z ∈ A"
                thus  "(z, a) ∈ r" 
                  using  `z ≠ a` `∀y∈A. y ≠ a  ⟶ (y,a) ∈ r` by auto
              next
                assume "z = x" 
                thus  "(z, a) ∈ r" using `(x, a) ∈ r` by auto
              qed
            qed
          qed
        qed
        thus "∃a. maximum (insert x A) a r" 
          using `a∈(insert x A)`  by(unfold maximum_def, auto)      
      qed
    qed
  qed
qed
  thus ?thesis using assms by auto
qed

lemma finiteness_union_finite_sets:
  fixes S :: "'a  ⇒  'a set" 
  assumes "∀x. finite (S x)" and "finite A"
  shows "finite (⋃a∈A. (S a))" using assms by auto

lemma uniqueness_level_aux:
  assumes "k>0"
  shows "(level A r n) ∩ (level A r (n+k)) = {}" 
proof(rule ccontr)
  assume  "level A r n ∩ level A r (n + k) ≠ {}" 
  hence  "∃x. x∈(level A r n) ∩ level A r (n + k)" by auto
  then obtain x where "x∈(level A r n) ∩ level A r (n + k)" by auto
  hence "x∈A ∧ height A x r = n" and "x∈A ∧ height A x r = n+k"
    by(unfold level_def, auto)
  thus False using `k>0` by auto
qed

lemma uniqueness_level:
  assumes "n≠m" 
  shows "(level A r n) ∩ (level A r m) = {}"
proof-
  have "n < m ∨ m < n" using assms by auto
  thus ?thesis
  proof(rule disjE)
    assume "n < m"
    hence "∃k. k>0 ∧ m=n+k" by arith
    thus ?thesis using uniqueness_level_aux[of _ A r] by auto
  next
    assume "m < n"
    hence "∃k. k>0 ∧ n=m+k" by arith
    thus ?thesis using  uniqueness_level_aux[of _ A r] by auto
  qed
qed
 
definition tree ::  "'a set ⇒ 'a rel ⇒ bool"
  where "tree A r  ≡
 r ⊆ A × A ∧ r≠{} ∧ (strict_part_order A r)  ∧  (∃a. minimum A a r) ∧
 (∀a∈A. finite (predecessors A a r) ∧ (total_on (predecessors A  a r) r))"

definition finite_tree::  "'a set ⇒ 'a rel ⇒ bool"
  where
"finite_tree A r  ≡ tree A r ∧ finite A"

abbreviation  infinite_tree::  "'a set ⇒ 'a rel ⇒ bool" 
  where
"infinite_tree A r  ≡  tree A r ∧ ¬ finite A"

definition enumerable_tree :: "'a set ⇒ 'a rel ⇒ bool"  where
 "enumerable_tree A r ≡ ∃g. enumeration (g:: nat ⇒'a)"

definition finitely_branching ::  "'a set ⇒ 'a rel ⇒ bool"
  where  "finitely_branching  A r ≡ (∀x∈A. finite (imm_successors A x r))"

definition sub_linear_order :: "'a set ⇒ 'a set ⇒ 'a rel ⇒ bool"
  where "sub_linear_order B A r  ≡  B⊆A ∧ (strict_part_order A r) ∧ (total_on B r)"

definition path ::  "'a set ⇒ 'a set ⇒ 'a rel ⇒ bool"
  where "path  B A r  ≡
 (sub_linear_order B A r) ∧
 (∀C. B ⊆ C ∧ sub_linear_order C A r ⟶ B = C)"

definition finite_path:: "'a set ⇒ 'a set ⇒ 'a rel ⇒ bool"
  where "finite_path B A r ≡  path  B A r ∧ finite B"

definition infinite_path:: "'a set ⇒ 'a set ⇒ 'a rel ⇒ bool"
  where "infinite_path B A r ≡  path  B A r ∧  ¬ finite B"

lemma tree: 
  assumes "tree A r"
  shows
  "r ⊆ A × A" and "r≠{}" 
  and  "strict_part_order A r"
  and  "∃a. minimum A a r" 
  and  "(∀a∈A. finite (predecessors A a r) ∧ (total_on (predecessors A  a r) r))"
  using `tree A r` by(unfold tree_def, auto)

lemma non_empty: 
  assumes "tree A r" shows "A≠{}"
proof-
  have "∃a. minimum A a r" using  `tree A r` tree[of A r] by auto
  hence "∃a. a∈A"  by(unfold minimum_def, auto)
  thus  "A≠{}" by auto
qed

lemma predecessors_spo:
  assumes "tree A r" 
  shows  "∀x∈A. strict_part_order (predecessors A x r) r"
proof- 
  have "irreflexive_on A r" and "transitive_on A r"  using `tree A r`
    by(unfold tree_def,unfold strict_part_order_def,auto) 
  thus ?thesis
proof(unfold strict_part_order_def)
  show "∀x∈A. irreflexive_on (predecessors A x r) r ∧
        transitive_on (predecessors A x r) r"
  proof
    fix x
    assume "x∈A"
    show "irreflexive_on (predecessors A x r) r ∧ transitive_on (predecessors A x r) r"
    proof-
      have 1: "irreflexive_on (predecessors A x r) r"
      proof(unfold irreflexive_on_def)
        show "∀y∈(predecessors A x r). (y, y) ∉ r"
        proof
          fix y
          assume "y∈(predecessors A x r)"
          hence "y∈A" by(unfold predecessors_def,auto)
          thus "(y, y) ∉ r" using `irreflexive_on A r` by(unfold irreflexive_on_def,auto)
        qed
      qed
      have 2: "transitive_on (predecessors A x r) r"
      proof(unfold transitive_on_def)
        let ?B= "(predecessors A x r)"
        show "∀w∈?B. ∀y∈?B. ∀z∈?B. (w, y) ∈ r ∧ (y, z) ∈ r ⟶ (w, z) ∈ r"
        proof
          fix w assume "w∈?B"
         show "∀y∈?B. ∀z∈?B. (w, y) ∈ r ∧ (y, z) ∈ r ⟶ (w, z) ∈ r"
         proof
           fix y assume "y∈?B"
           show "∀z∈?B. (w, y) ∈ r ∧ (y, z) ∈ r ⟶ (w, z) ∈ r"
           proof 
             fix z  assume "z∈?B"
             show "(w, y) ∈ r ∧ (y, z) ∈ r ⟶ (w, z) ∈ r"
             proof(rule impI)
               assume hip: "(w, y) ∈ r ∧ (y, z) ∈ r" 
               show "(w, z) ∈ r"
               proof-
                 have  "w∈A" and  "y∈A" and  "z∈A" using `w∈?B` `y∈?B` `z∈?B`
                   by(unfold predecessors_def,auto)
                 thus "(w, z) ∈ r"
                   using hip `transitive_on A  r` by(unfold transitive_on_def, blast)
                 qed
               qed
             qed
           qed
         qed
       qed
       show
        "irreflexive_on (predecessors A x r) r ∧ transitive_on (predecessors A x r) r"
       using 1 2 by auto
       qed
     qed
  qed
qed
       
lemma predecessors_maximum:
  assumes "tree A r" and  "minimum A a r"
  shows "∀x∈A. x≠a ⟶ (∃b. maximum (predecessors A x r) b r)"
proof
  fix x
  assume "x∈A"
  show "x≠a ⟶ (∃b. maximum (predecessors A x r) b r)"
  proof(rule impI)
    assume "x≠a"
    show "(∃b. maximum (predecessors A x r) b r)" 
    proof-
      have 1: "strict_part_order (predecessors A x r) r" 
        using  `tree A r` `x∈A`  predecessors_spo by auto
      have 2: "total_on (predecessors A x r) r" and 
           3: "finite (predecessors A x r)" and  "r ⊆ A × A"
        using  `tree A r` `x∈A` by(unfold tree_def, auto)
      have 4:  "(predecessors A x r)≠{}" 
        using  `r ⊆ A × A`  `minimum A a r`  `x∈A`  `x≠a` 
              min_predecessor[of A a] by auto
      have 5: "A≠{}" using `tree A r` non_empty by auto
      show "(∃b. maximum (predecessors A x r) b r)" 
        using 1 2 3 4 5  maximum_strict_part_order by auto
    qed
  qed
qed

lemma non_empty_preds_in_tree: 
  assumes  "tree A r"  and  "card (predecessors A x r) = n+1"
  shows  "x∈A"
proof- 
  have  "r ⊆ A × A"  using `tree A r` by(unfold tree_def, auto)
  have "(predecessors A x r) ≠ {}" using assms(2) by auto
  hence "∃y∈A. (y,x)∈r" by (unfold predecessors_def,auto)
  thus  "x∈A" using  `r ⊆ A × A` by auto
qed

lemma imm_predecessor:
  assumes  "tree A r"   
  and  "card (predecessors A x r) = n+1" and
  "maximum (predecessors A x r) b r"
  shows "height A b r = n"
proof- 
  have "transitive_on A r" and  "r ⊆ A × A" and  "irreflexive_on A r"
    using `tree A r`
    by (unfold tree_def, unfold strict_part_order_def, auto)
  have  "x∈A" using  assms(1) assms(2)  non_empty_preds_in_tree by auto
  have "strict_part_order (predecessors A x r) r"
    using `x∈A` `tree A r` predecessors_spo[of A r] by auto
  hence  "irreflexive_on (predecessors A x r) r" and
         "transitive_on (predecessors A x r) r"
    by(unfold strict_part_order_def, auto) 
  have "b∈(predecessors A x r)" 
    using `maximum (predecessors A x r) b r` by(unfold maximum_def, auto)
  have "total_on (predecessors A x r) r"
    using `x∈A` `tree A r` by(unfold tree_def, auto)
  have "card (predecessors A x r)>0 " using assms(2) by auto
  hence 1: "finite (predecessors A x r)"  using card_gt_0_iff by blast
  have  2: "b∈(predecessors A x r)" 
    using assms(3) by (unfold maximum_def,auto)
  hence "card ((predecessors A x r)-{b}) = n" 
    using 1  `card (predecessors A x r) = n+1`
    card_Diff_singleton[of b "(predecessors A x r)" ] by auto
  have "(predecessors A b r) = ((predecessors A x r)-{b})"
  proof(rule equalityI)
    show "(predecessors A b r) ⊆ (predecessors A x r - {b})" 
    proof
      fix y
      assume  "y∈ (predecessors A b r)"
      hence "y∈A" and  "(y,b)∈ r" by (unfold predecessors_def,auto)
      hence "y≠b" using `irreflexive_on A r` by(unfold irreflexive_on_def,auto)
      have "(b,x)∈r" using 2 by (unfold predecessors_def,auto)
      hence "b∈A"  using `r ⊆ A × A` by auto
      have "(y,x)∈ r" using `x∈A` `y∈A` `b∈A`  `(y,b)∈ r`  `(b,x)∈r` `transitive_on A r`
        by(unfold transitive_on_def, blast)    
      show "y∈(predecessors A x r - {b})" 
        using `y∈A` `(y,x)∈ r` `y≠b` by(unfold predecessors_def, auto)
    qed
  next
    show "(predecessors A x r - {b}) ⊆ (predecessors A b r)"
    proof
      fix y
      assume hip: "y∈(predecessors A x r - {b})" 
      hence "y≠b" and  "y∈A" by(unfold predecessors_def, auto)
      have "(y,b)∈ r" using hip `maximum (predecessors A x r) b r`
        by(unfold maximum_def,auto)
      thus "y∈ (predecessors A b r)" using `y∈A`
        by(unfold predecessors_def, auto)
    qed
  qed
  hence 3:  "card (predecessors A b r) = card (predecessors A x r - {b})" 
    by auto
  have "finite (predecessors A x r)" using `x∈A` `tree A r` by(unfold tree_def,auto)
  hence "card (predecessors A x r - {b}) = card (predecessors A x r)-1 " 
    using 2  card_Suc_Diff1 by auto
  hence "card (predecessors A b r) = n"
    using 3  `card (predecessors A x r) = n+1` by auto
  thus "height A b r = n" by (unfold height_def, auto)
qed
 
lemma height:
  assumes  "tree A r" and "height A x r = n+1"  
  shows "∃y. (y,x)∈r ∧ height A y r = n"
proof -
  have 1: "card (predecessors A x r) = n+1" 
    using assms(2) by (unfold height_def, auto)
  have "∃a. minimum A a r" using `tree A r` by(unfold tree_def, auto) 
  then obtain a where a: "minimum A a r"  by auto
  have  "strict_part_order A r" using  `tree A r` tree[of A r]  by auto
  hence  "height  A a r = 0" using a  height_minimum[of A r] by auto
  hence "x ≠ a" using assms(2) by auto
  have "x∈A"  using `tree A r`  1  non_empty_preds_in_tree by auto 
  hence "(∃b. maximum (predecessors A x r) b r)" 
    using `x ≠ a` `tree A r` a predecessors_maximum[of A r a] by auto
  then obtain b where b: "(maximum (predecessors A x r) b r)" by auto
  hence "(b,x)∈r" by(unfold maximum_def, unfold predecessors_def,auto)
  thus "∃y. (y,x)∈r ∧ height A y r = n"
    using  `tree A r` 1 b imm_predecessor[of A r] by auto 
qed

lemma level:
  assumes  "tree A r" and "x ∈ (level A r (n+1))"  
  shows "∃y. (y,x)∈r ∧ y ∈ (level A r n)"
proof-
  have "height A x r = n+1"
    using `x∈ (level A r (n+1))` by (unfold level_def, auto)
  hence "∃y. (y,x)∈r ∧ height A y r = n" 
    using `tree A r` height[of A r] by auto 
  then obtain y where y:  "(y,x)∈r ∧ height A y r = n" by auto
  have  "r ⊆ A × A"  using `tree A r` by(unfold tree_def,auto) 
  hence "y∈A" using y by auto
  hence "(y,x)∈r ∧ y ∈ (level A r n)" using y by(unfold level_def, auto)
  thus ?thesis by auto
qed
(*Para demostrar que en un árbol de ramificación los leveles son finites, se define
la siguiente función. *)
primrec set_nodes_at_level ::  "'a set ⇒ 'a rel ⇒ nat ⇒'a set" where
"set_nodes_at_level A r 0 = {a. (minimum A a r)}"
| "set_nodes_at_level A r (Suc n)  = (⋃a∈ (set_nodes_at_level A r n). imm_successors A a r)"

lemma set_nodes_at_level_zero_spo:
  assumes  "strict_part_order A r" and  "minimum A a r"
  shows "(set_nodes_at_level A r 0) = {a}"
proof-
  have "a∈(set_nodes_at_level A r 0)" using `minimum A a r` by auto
  hence 1: "{a} ⊆ (set_nodes_at_level A r 0)" by auto
  have 2:  "(set_nodes_at_level A r 0) ⊆ {a}"
  proof
    {fix x
    assume "x∈(set_nodes_at_level A r 0)"
    hence "minimum A x r" by auto
    hence "x=a" using assms  spo_uniqueness_min[of A r] by auto
    thus "x∈{a}" by auto}
  qed
  thus "(set_nodes_at_level A r 0) = {a}" using 1 2 by auto
qed

lemma height_level:
  assumes "strict_part_order A r"  and  "minimum A a r"
  and "x ∈ set_nodes_at_level A r n"
  shows "height A x r = n"
proof-
  have
 "⟦strict_part_order A r; minimum A a r; x ∈ set_nodes_at_level A r n⟧ ⟹ 
  height A x r = n" 
  proof(induct n arbitrary: x)
    case 0
    then show "height A x r = 0"
    proof-
      have "minimum A x r"  using `x ∈ set_nodes_at_level A r 0` by auto
      thus "height A x r = 0"
        using `strict_part_order A r`  height_minimum[of A r]
        by auto
    qed
  next
    case (Suc n)
    then show ?case 
    proof-
      have  "x∈ (⋃a ∈ (set_nodes_at_level A r n). (imm_successors A a r))"
        using Suc(4) by auto
      then  obtain a
        where hip1:  "a ∈ (set_nodes_at_level A r n)" and hip2: "x∈ (imm_successors A a r)" 
        by auto
      hence 1: "height A a r = n" using  Suc(1-3) by auto
      have "height A x r = (height A a r)+1" 
        using hip2 by(unfold imm_successors_def, auto)
      thus "height A x r = Suc n" using 1 by auto
    qed
  qed
  thus ?thesis using assms by auto
qed

lemma level_func_vs_level_def: 
  assumes  "tree A r"
  shows "set_nodes_at_level A r n = level A r n"   
proof(induct n)
  have 1: "strict_part_order A r" and
       2: "∀x∈A. finite (predecessors A x r)"
    using  `tree A r` tree[of A r] by auto 
  have "∃a. minimum A a r" using `tree A r` by(unfold tree_def, auto)
  then obtain a where a: "minimum A a r"  by auto
  case 0
  then show  "set_nodes_at_level A r 0 = level A r 0" 
  proof- 
    have "set_nodes_at_level A r 0 = {a}" using 1 a  set_nodes_at_level_zero_spo[of A r] by auto
    moreover 
    have "level A r 0 = {a}" using 1 2  a  zero_level[of A r] by auto
    ultimately
    show "set_nodes_at_level A r 0 = level A r 0" by auto
  qed
  next
    case (Suc n)
    assume  "set_nodes_at_level A r n = level A r n"
    show "set_nodes_at_level A r (Suc n) = level A r (Suc n)"
    proof(rule equalityI)
      show "set_nodes_at_level A r (Suc n) ⊆ level A r (Suc n)"
      proof(rule subsetI)
        fix x
        assume hip:  "x ∈ set_nodes_at_level A r (Suc n)" show "x ∈ level A r (Suc n)"
        proof- 
          have
          "set_nodes_at_level A r (Suc n) = (⋃a ∈ (set_nodes_at_level A r n). (imm_successors A a r))"
            by simp
          hence "x∈ (⋃a ∈ (set_nodes_at_level A r n). (imm_successors A a r))"
            using hip by auto 
          then obtain a where hip1: "a ∈ (set_nodes_at_level A r n)" and
            hip2:"x∈ (imm_successors A a r)" by auto
          have "(a,x)∈r ∧  height A x r = (height A a r)+1" 
            using hip2 by(unfold imm_successors_def, auto)
          moreover
          have "∃b. minimum A b r" using `tree A r` by(unfold tree_def, auto)
         then obtain b where b: "minimum A b r"  by auto
         have 1:  "r ⊆ A × A" and  "strict_part_order A r"
           using `tree A r` by(unfold tree_def, auto)     
         hence "height A a r = n" using b hip1  height_level[of A r] by auto
         ultimately
         have "(a,x)∈r ∧ height A x r = n+1" by auto
         hence "x∈A ∧ height A x r = n+1" using `r ⊆ A × A` by auto
         thus "x ∈ level A r (Suc n)" by(unfold level_def, auto)
       qed
     qed
  next
    show "level A r (Suc n) ⊆ set_nodes_at_level A r (Suc n)"
    proof(rule subsetI)
      fix x
      assume hip: "x ∈ level A r (Suc n)" show "x ∈ set_nodes_at_level A r (Suc n)"
      proof-
        have  1: "x∈A ∧ height A x r = n+1" using hip by(unfold level_def,auto)
        hence  "∃y. (y,x)∈r ∧ height A y r = n" 
        using assms height[of A r] by auto
        then obtain y where y1: "(y,x)∈r"  and y2: "height A y r = n" by auto
        hence "x ∈ (imm_successors A y r)" 
          using 1 by(unfold imm_successors_def, auto)
        moreover
        have  "r ⊆ A × A"  using `tree A r` by(unfold tree_def, auto)
        have "y∈A" using y1  `r ⊆ A × A` by auto
        hence "y∈ level A r n" using y2 by(unfold level_def, auto)
        hence "y∈ set_nodes_at_level A r n" using Suc by auto 
        ultimately
        show "x ∈ set_nodes_at_level A r (Suc n)" by auto
      qed
    qed
  qed
qed

lemma pertenece_level:
  assumes "x ∈ set_nodes_at_level A r n" 
  shows "x∈A" 
proof-
  have "x ∈ set_nodes_at_level A r n ⟹ x∈A"
  proof(induct n) 
    case 0
    show  "x ∈ A"  using  `x ∈ set_nodes_at_level A r 0` minimum_def[of A x r] by auto
  next
    case (Suc n)
    then show "x ∈ A"
    proof- 
      have "∃a ∈ (set_nodes_at_level A r n). x∈ imm_successors A a r"  
        using `x ∈ set_nodes_at_level A r (Suc n)` by auto  
      then obtain a  where  a1:  "a ∈ (set_nodes_at_level A r n)" and
        a2: "x∈ imm_successors A a r" by auto
      show "x ∈ A" using a2 imm_successors_def[of A a r] by auto   
    qed
  qed
  thus "x ∈ A" using assms by auto
qed

lemma finiteness_set_nodes_at_levela:
  assumes  "∀x∈A. finite (imm_successors A x r)" and "finite (set_nodes_at_level A r n)"
  shows "finite (⋃a∈ (set_nodes_at_level A r n). imm_successors A a r)"
proof  
  show "finite (set_nodes_at_level A r n)" using assms(2) by simp
next
  fix x
  assume hip:  "x ∈ set_nodes_at_level A r n" show  "finite (imm_successors A x r)"
  proof-  
    have "x∈A" using hip  pertenece_level[of x A r]  by auto 
    thus  "finite (imm_successors A x r)"  using assms(1) by auto 
  qed
qed

lemma finiteness_set_nodes_at_level:
  assumes "finite (set_nodes_at_level A r 0)" and  "finitely_branching A r"
  shows  "finite (set_nodes_at_level A r n)"
proof(induct n)
  case 0
  show "finite (set_nodes_at_level A r 0)" using assms  by auto
next
  case (Suc n)
  then show ?case
  proof -   
    have 1: "∀x∈A. finite (imm_successors A x r)"
      using assms by (unfold finitely_branching_def, auto)
    hence  "finite (⋃a∈ (set_nodes_at_level A r n). imm_successors A a r)"
      using Suc(1) finiteness_set_nodes_at_levela[of A r] by auto 
    thus "finite (set_nodes_at_level A r (Suc n))" by auto
  qed
qed

lemma finite_level:
  assumes  "tree A r" and "finitely_branching  A r" 
  shows  "finite (level A r n)" 
proof-
  have 1: "strict_part_order A r"  using `tree A r` tree[of A r] by auto
  have  "∃a. minimum A a r"  using `tree A r` tree[of A r] by auto
  then obtain a where "minimum A a r" by auto
  hence "finite (set_nodes_at_level A r 0)" 
    using 1  set_nodes_at_level_zero_spo[of A r] by auto
  hence "finite (set_nodes_at_level A r n)"
    using `finitely_branching  A r` finiteness_set_nodes_at_level[of A r] by auto
  thus  ?thesis using `tree A r` level_func_vs_level_def[of A r n] by auto
qed

lemma  finite_level_a:
  assumes "tree A r" and "∀n. finite (level A r n)"
  shows "finitely_branching A r"
proof(unfold finitely_branching_def)
  show  "∀x∈A. finite (imm_successors A x r)"
  proof
  fix x
  assume "x∈A"
  show "finite (imm_successors A x r)" using finitely_branching_def
  proof-
    let ?n = "(height A x r)"
    have "(imm_successors A x r) ⊆ (level A r (?n+1))"
      using imm_successors_def[of A x r] level_def[of A r "?n+1"] by auto 
    thus "finite (imm_successors A x r)"  using assms(2) by(simp add: finite_subset)   
  qed
qed
qed

lemma empty_predec: 
  assumes "∀x∈A. (x,y)∉r"  
  shows "predecessors A y r ={}" 
    using assms by(unfold predecessors_def, auto)

lemma level_element:
 "∀x∈A.∃n. x∈ level A r n"
proof
  fix x
  assume hip: "x∈A" show "∃n. x ∈ level A r n"
  proof-
    let ?n = "height A x r"
    have "x∈level A r ?n" using `x∈A`  by (unfold level_def, auto)
    thus "∃n. x ∈ level A r n" by auto 
  qed
qed

lemma union_levels:
  shows "A =(⋃n. level A r n)"
proof(rule equalityI)
  show "A ⊆ (⋃n. level A r n)"
  proof(rule subsetI)
    fix x
    assume hip: "x∈A" show "x∈(⋃n. level A r n)"
    proof-
      have "∃n. x∈ level A r n"  
        using hip level_element[of A] by auto
      then obtain n where  "x∈ level A r n" by auto
    thus ?thesis by auto 
  qed
qed
next
  show  "(⋃n. level A r n) ⊆ A"
  proof(rule subsetI)
    fix x
    assume hip:  "x ∈ (⋃n. level A r n)" show "x ∈ A"
    proof-
      obtain n where  "x∈ level A r n" using hip by auto 
      thus "x ∈ A" by(unfold level_def, auto)
    qed
  qed
qed

lemma path_to_node:
  assumes  "tree A r"  and  "x ∈ (level A r (n+1))" 
  shows "∀k.(0≤k ∧ k≤n)⟶ (∃y. (y,x)∈r ∧ y ∈ (level A r k))"
proof- 
  have "tree A r ⟹ x ∈ (level A r (n+1)) ⟹  
  ∀k.(0≤k ∧ k≤n)⟶ (∃y. (y,x)∈r ∧ y ∈ (level A r k))"
  proof(induction n arbitrary: x)
    have "r ⊆ A × A" and 1:  "strict_part_order A r" 
    and "∃a. minimum A a r"
    and 2: "∀x∈A. finite (predecessors A x r)"  
      using `tree A r` tree[of A r] by auto
    case 0
    show  "∀k. 0 ≤ k ∧ k ≤ 0 ⟶ (∃y. (y, x) ∈ r ∧ y ∈ level A r k)"
    proof
      fix k
      show "0 ≤ k ∧ k ≤ 0 ⟶ (∃y. (y, x) ∈ r ∧ y ∈ level A r k)"
      proof(rule impI)
        assume hip:  "0 ≤ k ∧ k ≤ 0"
        show "(∃y. (y, x) ∈ r ∧ y ∈ level A r k)" 
        proof-
          have "k=0" using hip  by auto
          thus "(∃y. (y, x) ∈ r ∧ y ∈ level A r k)"
            using `tree A r`  `x ∈ (level A r (0 + 1))` level[of A r ]  by auto
        qed      
      qed
    qed
    next
      case (Suc n)
      show "∀k. 0 ≤ k ∧ k ≤ Suc n ⟶ (∃y. (y, x) ∈ r ∧ y ∈ level A r k)"
  proof(rule allI, rule impI)
    fix k 
    assume hip:  "0 ≤ k ∧ k ≤ Suc n"
    show  "(∃y. (y, x) ∈ r ∧ y ∈ level A r k)"
    proof-
      have "(0 ≤ k ∧ k ≤ n) ∨ k = Suc n"  using hip by auto
      thus ?thesis
      proof(rule disjE)
        assume hip1:  "0 ≤ k ∧ k ≤ n"
        have "∃y. (y,x)∈r ∧ y ∈ (level A r (n+1))" 
        using `tree A r` level  `x ∈ level A r (Suc n + 1)` by auto
        then obtain y where y1: "(y,x)∈r" and y2: "y ∈ (level A r (n+1))" 
          by auto    
        have "∀k. 0 ≤ k ∧ k ≤ n ⟶ (∃z. (z, y) ∈ r ∧ z ∈ level A r k)" 
          using y2  Suc(1-3) by auto 
        hence "(∃z. (z, y) ∈ r ∧ z ∈ level A r k)" 
          using hip1 by auto
        then obtain z where  z1: "(z, y) ∈ r" and z2: "z ∈ (level A r k)" by auto
        have  "r ⊆ A × A" and "strict_part_order A r" 
          using  `tree A r` tree by auto
        hence "z∈A" and  "y∈A" and "x∈A"
          using `r ⊆ A × A` `(z, y) ∈ r` `(y,x)∈r` by auto
        have "transitive_on A r" using `strict_part_order A r`
          by(unfold strict_part_order_def, auto)
        hence "(z, x) ∈ r" using `z∈A` `y∈A` and `x∈A` `(z, y) ∈ r` `(y,x)∈r`
          by(unfold transitive_on_def, blast)
        thus "(∃y. (y, x) ∈ r ∧ y ∈ level A r k)"
          using z2 by auto
      next
        assume  "k = Suc n"
        thus  "∃y. (y,x)∈r ∧ y ∈ (level A r k)"
          using `tree A r` level `x ∈ level A r (Suc n + 1)` by auto
        qed
      qed
    qed
  qed
  thus ?thesis using assms by auto
qed

lemma set_nodes_at_level:  
  assumes "tree A r"  
  shows "(level A r (n+1))≠ {} ⟶ (∀k.(0≤k ∧ k≤n) ⟶ (level A r k)≠ {})"
proof(rule impI) 
  assume hip:  "(level A r (n+1))≠ {}"
    show  "(∀k.(0≤k ∧ k≤n) ⟶ (level A r k)≠ {})"
    proof-      
      have  "∃x. x∈(level A r (n+1))" using hip by auto  
      then obtain x where x: "x∈(level A r (n+1))" by auto
      thus ?thesis using assms path_to_node[of A r] by blast
    qed
  qed

lemma emptyness_below_height:
  assumes  "tree A r"  
  shows  "((level A r (n+1)) = {}) ⟶ (∀k. k>(n+1) ⟶ (level A r k) = {})"
proof(rule ccontr)
  assume hip: "¬ (level A r (n+1) = {} ⟶ (∀k>(n+1). level A r k = {}))"
  show False
  proof-
    have "((level A r (n+1)) = {}) ∧ ¬(∀k>(n+1). level A r k = {})" 
      using hip by auto
    hence 1: "(level A r (n+1)) = {}" and 2: "∃k>(n+1). (level A r k) ≠ {}"
      by auto
    obtain z where z1: "z>(n+1)" and z2: "(level A r z) ≠ {}"
      using 2 by auto
    have "z>0" using  `z>(n+1)` by auto 
    hence "(level A r ((z-1)+1)) ≠ {}"
      using z2 by simp
    hence "∀k.(0≤k ∧ k≤(z-1)) ⟶ (level A r k)≠ {}" 
      using  z2 `tree A r` set_nodes_at_level[of A r "z-1"]
      by auto
    hence  "(level A r (n+1)) ≠ {}"
      using `z>(n+1)` by auto
    thus False using 1 by auto
  qed
qed

lemma characterization_nodes_tree_finite_height:
  assumes "tree A r" and "∀k. k>m ⟶ (level A r k) = {}"
  shows "A = (⋃n∈{0..m}. level A r n)"
proof- 
  have a: "A = (⋃n. level A r n)" using  union_levels[of A r] by auto
  have "(⋃n. level A r n) = (⋃n∈{0..m}. level A r n)"
  proof(rule equalityI)
    show "(⋃n. level A r n) ⊆ (⋃n∈{0..m}.  level A r n)"
    proof(rule subsetI)
      fix x
      assume hip: "x∈(⋃n. level A r n)" 
      show "x∈(⋃n∈{0..m}. level A r n)"
      proof-
        have "∃n. x∈ level A r n"  
        using hip level_element[of A] by auto
        then obtain n where n: "x∈ level A r n" by auto
        have "n∈{0..m}"
        proof(rule ccontr)
          assume 1: "n ∉ {0..m}"
          show False
          proof-
            have "n > m" using 1 by auto
            thus False using assms(2) n by auto
          qed
        qed
        thus "x∈(⋃n∈{0..m}. level A r n)" using n by auto
      qed
    qed
  next
    show  "(⋃n∈{0..m}. level A r n) ⊆ (⋃n. level A r n)" by auto
  qed
  thus  "A = (⋃n∈{0..m}. level A r n)" using a by auto
qed

lemma finite_tree_if_fin_branches_and_fin_height:
  assumes "tree A r"  and  "finitely_branching  A r"
  and "∃n. (∀k. k>n ⟶ (level A r k) = {})"
  shows "finite A"
proof-
  obtain m where m: "(∀k. k>m ⟶ (level A r k) = {})" 
    using assms(3) by auto 
  hence 1: "A =(⋃n∈{0..m}. level A r n)"
    using  assms(1) assms(3) characterization_nodes_tree_finite_height[of A r m] by auto
  have "∀n. finite (level A r n)" 
    using assms(1-2) finite_level by auto
  hence "∀n∈{0..m}. finite (level A r n)" by auto
  hence "finite (⋃n∈{0..m}. level A r n)" by auto
  thus "finite A" using 1 by auto
qed

lemma all_levels_non_empty:
  assumes  "infinite_tree A r" and  "finitely_branching A r"
  shows "∀n. level A r n ≠ {}"
proof(rule ccontr)
  assume hip: "¬ (∀n. level A r n ≠ {})"
  show False
  proof-
    have "tree A r" using `infinite_tree A r` by auto
    have "(∃n. level A r n = {})" using hip by auto
    then obtain n where n: "level A r n = {}" by auto 
    thus False
    proof(cases n)
      case 0
      then show False
      proof-
        have "∃a. minimum A a r" using `tree A r` tree[of A r] by auto
        then obtain a where a:  "minimum A a r" by auto
        have " strict_part_order A r" 
        and "∀x∈A. finite (predecessors A x r)" 
          using  `tree A r` tree[of A r] by auto
        hence "level A r n = {a}" 
          using a `n=0` zero_level[of A r a] by auto
        thus False using `level A r n = {}` by auto
      qed
      next
        case (Suc nat)
        fix m
        assume hip: "n = Suc m" show False
        proof-
          have 1:  "level A r (Suc m) = {}"  
            using hip  n by auto
        have "(∀k. k>(m+1) ⟶ (level A r k) = {})" 
          using `tree A r` 1  emptyness_below_height[of A r m] by auto
        hence 1: "(∃n. ∀k. k>n ⟶ (level A r k) = {})" by auto
        hence 2: "finite A" 
          using `tree A r` 1 `finitely_branching  A r` finite_tree_if_fin_branches_and_fin_height[of A r] by auto
        have 3:  "¬ finite A" using `infinite_tree A r` by auto
        show False using 2 3 by auto
      qed
    qed
  qed
qed

lemma simple_cyclefree:
  assumes "tree A r" and "(x,z)∈r" and "(y,z)∈r" and "x≠y" 
  shows "(x,y)∈r ∨ (y,x)∈r"
proof-
  have "r ⊆ A × A" using `tree A r` by(unfold tree_def, auto)
  hence "x∈A" and  "y∈A" and  "z∈A" using  `(x,z)∈r` and `(y,z)∈r` by auto 
  hence 1: "x ∈ predecessors A z r" and 2: "y ∈ predecessors A z r"
    using assms by(unfold predecessors_def, auto)
  have "(total_on (predecessors A  z r) r)"
    using `tree A r` `z∈A` by(unfold tree_def, auto)
  thus ?thesis using 1 2 `x≠y`  total_on_def[of "predecessors A z r" r] by auto 
qed

lemma inclusion_predecessors:
  assumes  "r ⊆ A × A" and "strict_part_order A r" and "(x,y)∈r"
  shows "(predecessors A x r) ⊂ (predecessors A y r)"
proof-
  have "irreflexive_on A r" and "transitive_on A r" 
    using assms(2) by (unfold strict_part_order_def, auto) 
  have 1: "(predecessors A x r)⊆ (predecessors A y r)"
  proof(rule subsetI)
    fix z
    assume "z∈predecessors A x r"
    hence "z∈A" and "(z,x)∈r" by(unfold predecessors_def, auto)
    have "x∈A" and "y∈A"  using `(x,y)∈r` `r ⊆ A × A` by auto
    hence "(z,y)∈r"
      using `z∈A` `y∈A` `x∈A` `(z,x)∈r` `(x,y)∈r` `transitive_on A r` 
      by (unfold transitive_on_def, blast) 
    thus "z∈predecessors A y r" 
      using `z∈A` by(unfold predecessors_def, auto)
  qed
  have 2: "x∈predecessors A y r" 
    using `r ⊆ A × A` `(x,y)∈r` by(unfold predecessors_def, auto)
  have 3:  "x∉predecessors A x r"
  proof(rule ccontr)
    assume "¬ x ∉ predecessors A x r"
    hence "x ∈ predecessors A x r" by auto
    hence "x∈A ∧ (x,x)∈r"
      by(unfold predecessors_def, auto)
    thus False using `irreflexive_on A r`
      by (unfold irreflexive_on_def, auto)
  qed
  have "(predecessors A x r) ≠ (predecessors A y r)"
    using 2 3 by auto
  thus ?thesis using 1 by auto
qed

lemma different_height_finite_pred:
  assumes  "r ⊆ A × A" and "strict_part_order A r" and "(x,y)∈r" 
  and  "finite (predecessors A y r)"
  shows "height A x r < height A y r" 
proof- 
  have "card(predecessors A x r) < card(predecessors A y r)" 
    using assms  inclusion_predecessors[of r A x y] psubset_card_mono by auto
  thus ?thesis by(unfold height_def, auto)
qed

lemma different_levels_finite_pred:
  assumes  "r ⊆ A × A" and "strict_part_order A r" and "(x,y)∈r"
  and "x ∈ (level A r n)"  and  "y ∈ (level A r m)" 
  and  "finite (predecessors A y r)"
  shows "level A r n ≠ level A r m"
proof(rule ccontr)
  assume "¬ level A r n ≠ level A r m"
  hence "level A r n = level A r m"  by auto
  hence "x ∈ (level A r m)"  using `x ∈ (level A r n)` by auto
  hence 1:  "height A x r= m"  by(unfold level_def, auto)
  have "height A y r= m" using `y ∈ (level A r m)` by(unfold level_def, auto)
  hence "height A x r = height A y r" using 1 by auto
  thus False 
    using assms different_height_finite_pred[of r A x y] by (unfold level_def, auto)
qed

lemma less_level_pred_in_fin_pred: 
  assumes  "r ⊆ A × A" and "strict_part_order A r" 
  and "x ∈ predecessors A y r"  and "y ∈ (level A r n)"
  and  "x ∈ (level A r m)" 
  and "finite (predecessors A y r)"
  shows "m<n" 
proof-
  have "(x,y)∈r" using `(x ∈ predecessors A y r)`
    by (unfold predecessors_def, auto)
  thus ?thesis 
    using assms  different_height_finite_pred[of r A x y] by(unfold level_def, auto)
qed

lemma emptyness_inter_diff_levels_aux:
  assumes "tree A r" and "x∈(predecessors A z r)" 
  and "y∈(predecessors A z r)"
  and  "x≠y" and "x ∈ (level A r n)" and "y ∈ (level A r m)" 
  shows "level A r n ∩ level A r m = {}" 
proof-   
  have "(x,y)∈r ∨ (y,x)∈r"     
    using assms simple_cyclefree[of A] by(unfold predecessors_def, auto)
  thus "level A r n ∩ level A r m ={}"
  proof(rule disjE)
    assume  "(x, y) ∈ r" 
    have "r⊆ A × A" and 1: "strict_part_order A r"
      using  `tree A r` by(unfold tree_def,auto)
    hence "x∈A" and "y∈A"  and  2: "x∈(predecessors A y r)"
      using `(x, y) ∈ r`  by(unfold predecessors_def, auto)
    have 3: "finite (predecessors A y r)"
      using `y∈A`  `tree A r` by(unfold tree_def, auto) 
    hence  "n<m"
      using assms `r⊆ A × A` 1 2 3 less_level_pred_in_fin_pred[of r A x y m n]
      by auto
    hence "∃k>0. m=n+k" by arith
    then obtain k where k: "k>0" and m: "m=n+k" by auto
    thus ?thesis using uniqueness_level_aux[OF k, of A ]
      by auto
  next
    assume  "(y, x) ∈ r" 
    have "r⊆ A × A" and 1: "strict_part_order A r"
      using  `tree A r` by(unfold tree_def,auto)
    hence "x∈A" and "y∈A" and 2: "y∈(predecessors A x r)"
      using `(y, x) ∈ r`
      by(unfold predecessors_def, auto)
    have 3: "finite (predecessors A x r)" 
      using `x∈A` `tree A r`
      by(unfold tree_def, auto) 
    hence  "m<n" 
      using assms `r⊆ A × A` 1 2 3 less_level_pred_in_fin_pred[of r A y x n m]
      by auto
    hence "∃k>0. n=m+k" by arith
    then obtain k where k: "k>0" and m: "n=m+k" by auto
    thus ?thesis using  uniqueness_level_aux[OF k, of A] by auto
  qed
qed

lemma emptyness_inter_diff_levels:
  assumes "tree A r" and "(x,z)∈ r" and "(y,z)∈ r"
  and  "x≠y" and  "x ∈ (level A r n)" and "y ∈ (level A r m)" 
shows "level A r n ∩ level A r m = {}" 
proof-
  have "r ⊆ A × A"  using  `tree A r` tree by auto
  hence "x∈A" and  "y∈A"  using  `r ⊆ A × A`  `(x,z) ∈ r`  `(y,z)∈r` by auto
  hence "x∈(predecessors A z r)" and "y∈(predecessors A z r)" 
    using  `(x,z)∈ r` and `(y,z)∈ r` by(unfold predecessors_def, auto)
  thus ?thesis
    using assms  emptyness_inter_diff_levels_aux[of A r] by blast
qed

primrec disjunction_nodes :: "'a list  ⇒ 'a formula"  where
 "disjunction_nodes [] = FF"   
| "disjunction_nodes (v#D) = (atom v) ∨. (disjunction_nodes D)"

lemma truth_value_disjunction_nodes:
  assumes "v∈ set l" and "t_v_evaluation I (atom v) = Ttrue"
  shows "t_v_evaluation I (disjunction_nodes l) = Ttrue"
proof-
  have "v∈ set l ⟹  t_v_evaluation I (atom v) = Ttrue ⟹
  t_v_evaluation I (disjunction_nodes l) = Ttrue" 
  proof(induct l)
    case Nil
    then show ?case by auto
  next
    case (Cons a l)
    then show  "t_v_evaluation I (disjunction_nodes (a # l)) = Ttrue"
    proof-
      have "v = a ∨ v≠a" by auto
      thus  "t_v_evaluation I (disjunction_nodes (a # l)) = Ttrue"
      proof(rule disjE)
        assume "v = a"
        hence 1: "disjunction_nodes (a#l) = (atom v) ∨. (disjunction_nodes l)"
          by auto 
        have "t_v_evaluation I ((atom v) ∨. (disjunction_nodes l)) = Ttrue"  
          using Cons(3)  by(unfold t_v_evaluation_def,unfold v_disjunction_def, auto)
        thus ?thesis using 1  by auto
      next
        assume "v ≠ a"
        hence "v∈ set l" using Cons(2) by auto
        hence "t_v_evaluation I (disjunction_nodes l) = Ttrue"
          using Cons(1) Cons(3) by auto
        thus ?thesis
          by(unfold t_v_evaluation_def,unfold v_disjunction_def, auto)
      qed
    qed
  qed
  thus ?thesis using assms by auto
qed

lemma set_set_to_list1:
  assumes "tree A r" and  "finitely_branching A r" 
  shows "set (set_to_list (level A r n)) = (level A r n)"
  using assms finite_level[of A r n]  set_set_to_list by auto

lemma truth_value_disjunction_formulas:
  assumes  "tree A r" and  "finitely_branching A r"
  and  "v∈(level A r n) ∧ t_v_evaluation I (atom v) = Ttrue" 
  and  "F = disjunction_nodes(set_to_list (level A r n))" 
  shows "t_v_evaluation I  F = Ttrue"
proof- 
  have "set (set_to_list (level A r n)) = (level A r n)" 
    using set_set_to_list1 assms(1-2) by auto
  hence "v∈ set (set_to_list (level A r n))"
    using assms(3) by auto
  thus "t_v_evaluation I F = Ttrue"
    using assms(3-4) truth_value_disjunction_nodes by auto
qed

definition ℱ :: "'a set ⇒ 'a rel ⇒ ('a formula) set"  where
   "ℱ A r  ≡ (⋃n. {disjunction_nodes(set_to_list (level A r n))})"

definition 𝒢 ::  "'a set ⇒ 'a rel ⇒ ('a formula) set"  where
   "𝒢 A r ≡ {(atom u) →. (atom v) |u v. u∈A ∧ v∈A ∧ (v,u)∈ r}" 

definition ℋn :: "'a set ⇒ 'a rel ⇒ nat ⇒ ('a formula) set"  where
   "ℋn A r n ≡ {¬.((atom u) ∧. (atom v))
                         |u v . u∈(level A r n) ∧ v∈(level A r n) ∧ u≠v }"
definition ℋ  :: "'a set ⇒ 'a rel ⇒ ('a formula) set"  where
 "ℋ A r  ≡ ⋃n. ℋn A r n"

definition 𝒯 :: "'a set ⇒ 'a rel ⇒ ('a formula) set"  where
   "𝒯 A r  ≡ (ℱ A r) ∪ (𝒢 A r) ∪ (ℋ A r)" 

primrec nodes_formula :: "'v formula  ⇒ 'v set" where
  "nodes_formula FF = {}"
| "nodes_formula TT = {}"
| "nodes_formula (atom P) =  {P}"
| "nodes_formula (¬. F) = nodes_formula F"
| "nodes_formula (F ∧. G) = nodes_formula F ∪ nodes_formula G"
| "nodes_formula (F ∨. G) = nodes_formula F ∪ nodes_formula G"
| "nodes_formula (F →.G) = nodes_formula F ∪ nodes_formula G"

definition nodes_set_formulas :: "'v formula set  ⇒ 'v set"  where
"nodes_set_formulas S = (⋃F∈ S. nodes_formula F)"

definition maximum_height:: "'v set ⇒'v rel ⇒ 'v  formula  set  ⇒  nat"  where
 "maximum_height A r S =  Max (⋃x∈nodes_set_formulas S. {height A x r})"

lemma node_formula:
  assumes "v ∈ set l" 
  shows "v ∈ nodes_formula (disjunction_nodes l)" 
proof-
  have "v ∈ set l ⟹ v ∈ nodes_formula (disjunction_nodes l)" 
  proof(induct l)
    case Nil
    then show ?case by auto
  next
    case (Cons a l)  
    show "v ∈ nodes_formula (disjunction_nodes (a # l))"  
   proof-
     have "v = a ∨ v≠a" by auto
     thus "v ∈ nodes_formula (disjunction_nodes (a # l))"
     proof(rule disjE)
       assume "v = a"
       hence 1: "disjunction_nodes (a#l) = (atom v) ∨. (disjunction_nodes l)"
         by auto 
       have "v ∈ nodes_formula ((atom v) ∨. (disjunction_nodes l))" by auto 
       thus ?thesis using 1  by auto
     next
       assume "v ≠ a"
       hence "v∈ set l" using Cons(2) by auto
       hence "v ∈ nodes_formula (disjunction_nodes l)"
         using Cons(1) Cons(2) by auto
       thus ?thesis by auto
     qed
   qed
 qed
  thus ?thesis using assms by auto
qed 

lemma node_disjunction_formulas:
  assumes  "tree A r" and  "finitely_branching A r" and "v∈(level A r n)" 
  and  "F = disjunction_nodes(set_to_list (level A r n))" 
  shows  "v ∈ nodes_formula F"
proof- 
  have "set (set_to_list (level A r n)) = (level A r n)" 
    using set_set_to_list1 assms(1-2) by auto
  hence "v∈ set (set_to_list (level A r n))" 
    using assms(3) by auto
  thus "v ∈ nodes_formula F"
    using assms(3-4)  node_formula  by auto
qed

fun node_sig_level_max:: "'v set ⇒ 'v rel ⇒ 'v formula set  ⇒ 'v" 
  where "node_sig_level_max A r S = 
  (SOME u. u ∈ (level A r ((maximum_height A r S)+1)))"

lemma node_level_maximum:  
  assumes "infinite_tree A r" and  "finitely_branching A r"
  shows "(node_sig_level_max A r S) ∈  (level A r ((maximum_height A r S)+1))" 
proof-
  have  "∃u. u ∈ (level A r ((maximum_height A r S)+1))"
    using assms  all_levels_non_empty[of A r] by (unfold level_def, auto)
  then obtain u where u: "u ∈ (level A r (( maximum_height A r S)+1))" by auto
  hence "(SOME u. u ∈ (level A r ((maximum_height A r S)+1))) ∈ (level A r ((maximum_height A r S)+1))" 
    using someI by auto
  thus ?thesis by auto 
qed

fun path_interpretation :: "'v set ⇒'v rel ⇒ 'v ⇒ ('v  ⇒  v_truth)"  where
"path_interpretation A r u = (λv. (if (v,u)∈r  then Ttrue else Ffalse))"

lemma finiteness_nodes_formula:
 "finite (nodes_formula F)" by(induct F, auto)

lemma finiteness_set_nodes:
  assumes "finite S" 
  shows  "finite (nodes_set_formulas S)" 
  using assms finiteness_nodes_formula 
  by (unfold nodes_set_formulas_def, auto)

lemma maximum1:
  assumes  "finite S" and "u ∈ nodes_set_formulas S"
  shows "(height A u r)  ≤ (maximum_height A r S)" 
proof-  
  have "(height A u r) ∈ ( ⋃x∈nodes_set_formulas S. {height A x r})" 
    using assms(2) by auto
  thus "(height A u r)  ≤ (maximum_height A r S)"
    using `finite S` finiteness_set_nodes[of S] 
    by(unfold maximum_height_def, auto) 
qed

lemma value_path_interpretation:
  assumes "t_v_evaluation (path_interpretation A r v) (atom u) = Ttrue"
  shows "(u,v)∈r"
proof(rule ccontr)
  assume "(u, v) ∉ r"
  hence "t_v_evaluation (path_interpretation A r v) (atom u) = Ffalse"
    by(unfold t_v_evaluation_def, auto) 
  thus False using assms by auto
qed

lemma satisfiable_path:
  assumes "infinite_tree A r"
  and  "finitely_branching A r" and  "S ⊆ (𝒯 A r)" 
  and "finite S" 
shows  "satisfiable S"
proof-
  let ?m = "(maximum_height A r S)+1"
  let ?level = "level A r ?m"
  let ?u = "node_sig_level_max A r S" 
  have 1: "tree A r" using `infinite_tree A r` by auto
  have  "r ⊆ A × A" and "strict_part_order A r" 
    using  `tree A r` tree by auto
  have "transitive_on A r" 
    using `strict_part_order A r`
    by(unfold strict_part_order_def, auto) 
  have "∃u. u ∈?level" 
    using assms(1-2) node_level_maximum by auto
  then obtain u where u: "u ∈ ?level"  by auto
  hence levelu:  "?u ∈ ?level"
    using someI by auto
  hence "?u∈A" by(unfold level_def, auto)
  have "(path_interpretation A r ?u) model S"
  proof(unfold model_def)
    show "∀F∈S. t_v_evaluation (path_interpretation A r ?u) F = Ttrue"
    proof 
      fix F assume "F ∈ S"
      show  "t_v_evaluation (path_interpretation A r ?u) F  = Ttrue"
      proof-        
        have "F ∈ (ℱ A r) ∪ (𝒢 A r) ∪ (ℋ A r)" 
        using `S ⊆  𝒯 A r` `F ∈ S` assms(2)  by(unfold 𝒯_def,auto) 
        hence  "F ∈ (ℱ A r) ∨ F ∈ (𝒢 A r) ∨ F ∈ (ℋ A r)" by auto 
        thus ?thesis
        proof(rule disjE)
          assume "F ∈ (ℱ A r)"
          hence "∃n. F = disjunction_nodes(set_to_list (level A r n))" 
            by(unfold ℱ_def,auto)
          then obtain n
            where n: "F = disjunction_nodes(set_to_list (level A r n))" 
            by auto
          have "∃v. v∈(level A r n)" 
            using  assms(1-2) all_levels_non_empty[of A r] by auto 
          then obtain v where v: "v ∈ (level A r n)" by auto      
          hence  "v ∈ nodes_formula F" 
            using n node_disjunction_formulas[OF 1 assms(2) v, of F ]
            by auto
          hence a: "v ∈ nodes_set_formulas S" 
            using `F ∈ S`  by(unfold nodes_set_formulas_def, blast)
          hence b: "(height A v r) ≤ (maximum_height A r S)" 
            using `finite S`  maximum1[of S v] by auto
          have "(height A v r) = n" 
            using v by(unfold level_def, auto) 
          hence  "n < ?m" 
            using `finite S` a   maximum1[of S v A r]
            by(unfold maximum_height_def, auto)         
          hence "(∃y. (y,?u)∈r ∧ y ∈ (level A r n))" 
            using levelu `tree A r` path_to_node[of A r]
            by auto
          then obtain y where y1: "(y,?u)∈r" and y2: "y ∈ (level A r n)"
            by auto
          hence "t_v_evaluation (path_interpretation A r ?u) (atom y) = Ttrue" 
            by auto
          thus "t_v_evaluation (path_interpretation A r ?u) F = Ttrue"
            using 1 assms(2) y2 n  truth_value_disjunction_formulas[of A r y]
            by auto
        next
          assume  "F ∈ 𝒢 A r ∨ F ∈ ℋ A r"
          thus "t_v_evaluation (path_interpretation A r ?u) F = Ttrue"
          proof(rule disjE)
            assume  "F ∈ 𝒢 A r"
            hence "∃u. ∃v. u∈A ∧ v∈A  ∧ (v,u)∈ r  ∧
                  (F = (atom u) →. (atom v))"
              by (unfold  𝒢_def, auto)
            then obtain u v where "u∈A" and "v∈A" and "(v,u)∈ r" 
            and F: "(F = (atom u) →. (atom v))" by auto
            show "t_v_evaluation (path_interpretation A r ?u) F = Ttrue"  
            proof(rule ccontr)
              assume "¬(t_v_evaluation (path_interpretation A r ?u) F = Ttrue)" 
              hence "t_v_evaluation (path_interpretation A r ?u) F = Ffalse"
                using Bivaluation by auto
              hence "t_v_evaluation (path_interpretation A r ?u) (atom u) =  Ttrue ∧
              t_v_evaluation (path_interpretation A r ?u) (atom v) =  Ffalse" 
                using F  eval_false_implication by blast
              hence 1: "t_v_evaluation (path_interpretation A r ?u) (atom u) =  Ttrue"
              and   2: "t_v_evaluation (path_interpretation A r ?u) (atom v) =  Ffalse"
                by auto
              have "(u,?u)∈r" using 1 value_path_interpretation by auto
              hence "(v,?u)∈ r" 
                using  `u∈A` `v∈A` `?u∈A` `(v,u)∈ r` `transitive_on A r` 
                by(unfold transitive_on_def, blast)
              hence "t_v_evaluation (path_interpretation A r ?u) (atom v) =  Ttrue" 
                by auto
              thus False using 2 by auto
            qed
          next
            assume  "F ∈ ℋ A r" 
            hence "∃n. F ∈ ℋn A r n" by(unfold  ℋ_def, auto)
            then obtain n where  "F ∈ ℋn A r n" by auto
            hence
            "∃u. ∃v. F = ¬.((atom u) ∧. (atom v)) ∧ u∈(level A r n) ∧
             v∈(level A r n) ∧ u≠v"
              by(unfold ℋn_def, auto)  
            then obtain u v where F: "F = ¬.((atom u) ∧. (atom v))" 
            and "u∈(level A r n)" and "v∈(level A r n)" and "u≠v"
              by auto
            show "t_v_evaluation (path_interpretation A r ?u) F = Ttrue"  
            proof(rule ccontr)
              assume "t_v_evaluation (path_interpretation A r ?u) F ≠ Ttrue"
              hence "t_v_evaluation (path_interpretation A r ?u) F = Ffalse"
                using Bivaluation by auto
              hence
              "t_v_evaluation (path_interpretation A r ?u)((atom u) ∧.
               (atom v)) = Ttrue" 
                using F  NegationValues1 by blast
              hence "t_v_evaluation (path_interpretation A r ?u)(atom u) = Ttrue ∧
              t_v_evaluation (path_interpretation A r ?u)(atom v) = Ttrue"
                using ConjunctionValues by blast
              hence "(u,?u)∈r" and  "(v,?u)∈r"
                using  value_path_interpretation by auto
              hence a: "(level A r n) ∩ (level A r n) = {}"
                using `tree A r`  `u∈(level A r n)`  `v∈(level A r n)`  `u≠v`
                emptyness_inter_diff_levels[of A r]
                by blast
              have "(level A r n) ≠ {}" 
                using  `v∈(level A r n)` by auto           
              thus False using a by auto 
            qed
          qed
        qed
      qed
    qed
  qed
  thus "satisfiable S" by(unfold satisfiable_def, auto)
qed

definition ℬ:: "'a set ⇒ ('a  ⇒ v_truth) ⇒ 'a set" where
"ℬ A I  ≡ {u|u. u∈A ∧ t_v_evaluation I (atom u) = Ttrue}"

lemma value_disjunction_list1:
  assumes "t_v_evaluation I (disjunction_nodes (a # l)) = Ttrue"
  shows "t_v_evaluation I (atom a) = Ttrue ∨ t_v_evaluation I (disjunction_nodes l) = Ttrue" 
proof-
  have "disjunction_nodes (a # l) = (atom a) ∨. (disjunction_nodes l)"
    by auto
  hence "t_v_evaluation I ((atom a) ∨. (disjunction_nodes l)) = Ttrue" 
    using assms by auto
  thus ?thesis using DisjunctionValues by blast
qed

lemma value_disjunction_list:
  assumes "t_v_evaluation I (disjunction_nodes l) = Ttrue"
  shows "∃x. x ∈ set l ∧ t_v_evaluation I (atom x) = Ttrue" 
proof-
  have "t_v_evaluation I (disjunction_nodes l) = Ttrue ⟹
  ∃x. x ∈ set l ∧  t_v_evaluation I (atom x) = Ttrue" 
  proof(induct l)
    case Nil
    then show ?case by auto
  next   
    case (Cons a l)  
    show  "∃x. x ∈ set (a # l) ∧ t_v_evaluation I (atom x) = Ttrue"  
    proof-
      have "t_v_evaluation I (atom a) = Ttrue ∨ t_v_evaluation I (disjunction_nodes l)=Ttrue" 
        using Cons(2) value_disjunction_list1[of I] by auto      
      thus ?thesis
    proof(rule disjE)
      assume "t_v_evaluation I (atom a) = Ttrue"
      thus ?thesis by auto
    next
      assume "t_v_evaluation I (disjunction_nodes l) = Ttrue" 
      thus ?thesis
        using Cons by auto    
    qed
  qed
qed
  thus ?thesis using assms by auto
qed 

lemma intersection_branch_set_nodes_at_level:
  assumes "infinite_tree A r" and "finitely_branching A r" 
  and I: "∀F ∈ (ℱ A r). t_v_evaluation I F = Ttrue"
shows "∀n. ∃x. x ∈ level A r n ∧ x ∈ (ℬ A I)" using all_levels_non_empty
proof- 
  fix n 
  have "∀n. t_v_evaluation I (disjunction_nodes(set_to_list (level A r n))) = Ttrue"
    using I by (unfold ℱ_def, auto)
  hence 1:
  "∀n. ∃x. x ∈ set (set_to_list (level A r n)) ∧ t_v_evaluation I (atom x) = Ttrue"
    using value_disjunction_list by auto
  have "tree A r" 
    using `infinite_tree A r`by auto
  hence "∀n. set (set_to_list (level A r n)) = level A r n" 
    using assms(1-2)  set_set_to_list1 by auto
  hence  "∀n. ∃x. x ∈ level A r n ∧  t_v_evaluation I (atom x) = Ttrue"
    using 1  by auto
  hence  "∀n. ∃x. x ∈ level A r n ∧ x∈A ∧ t_v_evaluation I (atom x) = Ttrue" 
    by(unfold level_def, auto)
  thus ?thesis using ℬ_def[of A I] by auto
qed

lemma intersection_branch_emptyness_below_height:
  assumes I:  "∀F ∈ (ℋ A r). t_v_evaluation I F = Ttrue" 
  and "x∈(ℬ A I)"  and  "y∈(ℬ A I)"  and  "x ≠ y" and  n: "x ∈ level A r n"
  and m: "y ∈ level A r m" 
shows  "n ≠ m"
proof(rule ccontr)
  assume "¬ n ≠ m"
  hence "n=m" by auto
  have "x∈A" and  "y∈A" and v1: "t_v_evaluation I (atom x) = Ttrue" 
  and v2: "t_v_evaluation I (atom y) = Ttrue" 
    using  `x∈(ℬ A I)` `y∈(ℬ A I)`  by(unfold ℬ_def, auto) 
  have "¬.((atom x) ∧. (atom y)) ∈ (ℋn A r n)" 
    using `x∈A`   `y∈A`  `x ≠ y` n m `n=m`
    by(unfold ℋn_def, auto)             
  hence "¬.((atom x) ∧. (atom y)) ∈ (ℋ A r)"
    by(unfold ℋ_def, auto)                   
  hence "t_v_evaluation I (¬.((atom x) ∧. (atom y))) = Ttrue"
    using I by auto
  moreover                  
  have "t_v_evaluation I ((atom x) ∧. (atom y)) = Ttrue"
    using v1 v2 v_conjunction_def by auto
  hence "t_v_evaluation I (¬.((atom x) ∧. (atom y))) = Ffalse" 
    using v_negation_def by auto 
  ultimately
  show False by auto
qed

lemma intersection_branch_level: 
  assumes  "infinite_tree A r" and "finitely_branching A r" 
  and I: "∀F ∈ (ℱ A r) ∪ (ℋ A r). t_v_evaluation I F = Ttrue"
shows "∀n. ∃u. (ℬ A I) ∩  level A r n = {u}"
proof
  fix n 
  show "∃u. (ℬ A I) ∩ level A r n = {u}" 
  proof-
    have "∃u. u ∈ level A r n ∧ u ∈ (ℬ A I)" 
      using assms intersection_branch_set_nodes_at_level[of A r I] by auto
    then obtain u where u: "u ∈ level A r n ∧ u∈(ℬ A I)" by auto
    hence 1:  "{u} ⊆ (ℬ A I) ∩ level A r n" by blast
    have 2:  "(ℬ A I) ∩ level A r n ⊆ {u}"
    proof(rule subsetI)
      fix x
      assume  "x∈(ℬ A I) ∩ level A r n"
      hence 2: "x∈(ℬ A I) ∧ x∈ level A r n"  by auto
      have "u = x"
      proof(rule ccontr)
        assume "u ≠ x"
        hence "n≠n" 
          using u 2 I intersection_branch_emptyness_below_height[of A r] by blast
        thus False by auto
      qed
      thus "x∈{u}" by auto
    qed
    have "(ℬ A I) ∩ level A r n = {u}"
      using 1 2 by auto
    thus "∃u.(ℬ A I) ∩  level A r n = {u}"  by auto
  qed
qed

lemma predecessor_in_branch:
  assumes I:  "∀F ∈ (𝒢 A r). t_v_evaluation I F = Ttrue" 
  and "y∈(ℬ A I)"  and  "(x,y)∈ r" and "x∈A" and "y∈A"
shows "x∈(ℬ A I)"
proof- 
  have "(atom y) →. (atom x)∈ 𝒢 A r" 
    using `x∈A`  `y∈A`  `(x, y)∈r` by (unfold  𝒢_def, auto)
  hence "t_v_evaluation I ((atom y) →. (atom x)) = Ttrue"
    using I by auto
  moreover
  have "t_v_evaluation I (atom y) = Ttrue" 
    using  `y∈(ℬ A I)` by(unfold ℬ_def, auto)
  ultimately
  have "t_v_evaluation I (atom x) = Ttrue"
    using v_implication_def by  auto
  thus  "x∈(ℬ A I)" using  `x∈A`  by(unfold ℬ_def, auto) 
qed

lemma is_path: 
  assumes  "infinite_tree A r" and "finitely_branching A r" 
  and I: "∀F ∈ (𝒯 A r). t_v_evaluation I F = Ttrue" 
shows "path (ℬ A I) A r"
proof(unfold path_def)
  let ?B = "(ℬ A I)" 
  have "tree A r" 
  using  `infinite_tree A r` by auto
  have "∀F ∈ (ℱ A r) ∪ (𝒢 A r) ∪ (ℋ A r). t_v_evaluation I F = Ttrue"
    using I by(unfold 𝒯_def)
  hence I1:  "∀F ∈ (ℱ A r). t_v_evaluation I F = Ttrue" 
  and   I2:  "∀F ∈ (𝒢 A r). t_v_evaluation I F = Ttrue"
  and   I3:  "∀F ∈ (ℋ A r). t_v_evaluation I F = Ttrue" 
    by auto 
  have 0: "sub_linear_order ?B A r"
  proof(unfold sub_linear_order_def)
    have 1: "?B ⊆ A"  by(unfold ℬ_def, auto)
    have 2: "strict_part_order A r" 
      using `tree A r` tree[of A r] by auto
    have "total_on ?B r"
    proof(unfold total_on_def)
      show "∀x∈?B. ∀y∈?B. x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r"
      proof
        fix x
        assume "x∈?B" 
        show "∀y∈?B. x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r"
        proof              
          fix y
          assume "y∈?B"
          show "x ≠ y ⟶ (x, y) ∈ r ∨ (y, x) ∈ r" 
          proof(rule impI)
            assume "x ≠ y" 
            have "x∈A" and "y∈A" and v1: "t_v_evaluation I (atom x) = Ttrue" 
            and v2: "t_v_evaluation I (atom y) = Ttrue" 
              using `x∈?B` `y∈?B`  by(unfold ℬ_def, auto)
            have "(∃n. x ∈ level A r n)" and "(∃m. y ∈ level A r m)" 
              using `x∈A` and `y∈A` level_element[of A r]
              by auto
            then obtain n m
            where n: "x ∈ level A r n" and m: "y ∈ level A r m"
              by auto             
            have "n≠m"
              using I3 `x∈?B` `y∈?B` `x ≠ y` n m 
                    intersection_branch_emptyness_below_height[of A r]
              by auto                
            hence "n<m ∨ m<n" by auto
            thus "(x, y) ∈ r ∨ (y, x) ∈ r" 
            proof(rule disjE)
              assume  "n < m"  
              have "(x, y) ∈ r"
              proof(rule ccontr)
                assume "(x, y) ∉ r"
                have "∃z. (z, y)∈r ∧ z ∈ level A r n" 
                  using `tree A r` `y ∈ level A r m` `n < m`
                         path_to_node[of A r y "m-1"]
                  by auto 
                then obtain z where z1: "(z, y)∈r" and z2: "z ∈ level A r n"
                  by auto 
                have "z∈A" using  `tree A r` tree z1 by auto
                hence "z∈(ℬ A I)" 
                  using I2 `y∈A` `y∈?B` `(z, y)∈r` predecessor_in_branch[of A r I y z]
                  by auto
                have "x≠z" using `(x, y) ∉ r` `(z, y)∈r` by auto  
                hence "n≠n"
                  using I3 `x∈?B` `z∈?B` n z2  intersection_branch_emptyness_below_height[of A r]
                  by blast  
                thus False by auto 
              qed
              thus "(x, y) ∈ r ∨ (y, x) ∈ r" by auto
            next
              assume "m < n"
              have "(y, x) ∈ r"
              proof(rule ccontr)
                assume "(y, x) ∉ r"
                have "∃z. (z, x)∈r ∧ z ∈ level A r m" 
                  using `tree A r`  `x ∈ level A r n`  `m < n`
                         path_to_node[of A r x "n-1"]
                  by auto 
                  then obtain z where z1: "(z, x)∈r" and z2: "z ∈ level A r m"
                  by auto 
                have "z∈A" using  `tree A r` tree z1 by auto
                hence  "z∈(ℬ A I)" 
                  using I2 `x∈A` `x∈?B` `(z, x)∈r` predecessor_in_branch[of A r I x z]
                  by auto
                have "y≠z" using `(y, x) ∉ r` `(z, x)∈r` by auto  
                hence "m≠m"
                  using I3 `y∈?B` `z∈?B` m z2 intersection_branch_emptyness_below_height[of A r ]
                  by blast
                thus False by auto 
              qed
              thus "(x, y) ∈ r ∨ (y, x) ∈ r" by auto
            qed
          qed
        qed
      qed
    qed
    thus 3: "?B ⊆ A ∧ strict_part_order A r ∧ total_on ?B r"
      using 1 2 by auto             
  qed             
  have 4: "(∀C. ?B ⊆ C ∧ sub_linear_order C A r ⟶ ?B = C)"               
  proof
    fix C
    show "?B ⊆ C ∧ sub_linear_order C A r ⟶ ?B = C"
    proof(rule impI)
      assume "?B ⊆ C ∧ sub_linear_order C A r"
      hence "?B ⊆ C" and  "sub_linear_order C A r" by auto
      have "C ⊆ ?B"           
      proof(rule subsetI)
          fix x
          assume "x∈ C"
        have "C ⊆ A"
          using `sub_linear_order C A r`
         by(unfold sub_linear_order_def, auto)
        hence "x∈A" using `x∈C` by auto
        have "∃n. x∈level A r n" 
          using `x∈A` level_element[of A] by auto
        then obtain n where n: "x∈level A r n" by auto
        have "∃u. (ℬ A I) ∩ level A r n = {u}"
          using assms(1,2) I1 I3 intersection_branch_level[of A r]
          by blast
        then obtain u where i: "(ℬ A I) ∩ level A r n = {u}" 
          by auto
        hence "u∈A" and u: "u ∈ level A r n"
         by(unfold level_def, auto)
        have "x=u" 
        proof(rule ccontr)               
          assume hip: "x≠u" 
          have "u∈(ℬ A I)" using i by auto
          hence "u∈C" using `?B ⊆ C` by auto
          have "total_on C r"
            using `sub_linear_order C A r` sub_linear_order_def[of C A r]
            by blast         
          hence "(x,u)∈r ∨ (u,x)∈r" 
            using hip `x∈C` `u∈C` `sub_linear_order C A r`
            by(unfold total_on_def,auto)
          thus False
          proof(rule disjE)
            assume "(x,u)∈r"               
            have "r ⊆ A × A" and "strict_part_order A r" 
            and "finite (predecessors A u r)"
              using `u∈A` `tree A r` tree[of A r] by auto
            hence  "(level A r n) ≠ (level A r n)" 
              using `(x,u)∈r` `x ∈ level A r n` `u ∈ level A r n` 
                    different_levels_finite_pred[of r A ] by blast
            thus False by auto
          next
            assume "(u,x)∈r"               
            have "r ⊆ A × A" and "strict_part_order A r" 
            and "finite (predecessors A x r)"
              using `x∈A` `tree A r` tree[of A r]  by auto
            hence "(level A r n) ≠ (level A r n)" 
              using `(u,x)∈r` `u ∈ level A r n` `x ∈ level A r n`
                    different_levels_finite_pred[of r A ] by blast
            thus False by auto
          qed
        qed          
        thus "x ∈ ?B" using i by auto
      qed
      thus  "?B = C"  using `?B ⊆ C` by blast
    qed
  qed
  thus "sub_linear_order (ℬ A I) A r ∧
          (∀C. ℬ A I ⊆ C ∧ sub_linear_order C A r ⟶ ℬ A I = C)"
    using `sub_linear_order (ℬ A I) A r` by auto
qed

lemma surjective_infinite:
  assumes  "∃f:: 'a ⇒ nat. ∀n. ∃x∈A. n = f(x)"
  shows "infinite A"
proof(rule ccontr)
  assume "¬ infinite A"
  hence "finite A" by auto
  hence "∃n. ∃g. A = g ` {i::nat. i < n}"
    using finite_imp_nat_seg_image_inj_on[of A] by auto 
  then obtain n g where g: "A = g ` {i::nat. i < n}" by auto
  obtain f where  "(∀n. ∃x∈A. n = (f:: 'a ⇒  nat)(x))" 
    using assms by auto
  hence "∀m. ∃k∈{i::nat. i < n}. m =(f ∘ g)(k)"
    using g  by auto
  hence  "(UNIV :: nat set)  = (f ∘ g) ` {i::nat. i < n}"
    by blast
  hence  "finite (UNIV :: nat set)" 
    using nat_seg_image_imp_finite by blast 
  thus False by auto
qed

lemma family_intersection_infinita:
  fixes P :: " nat ⇒ 'a set"
  assumes "∀n. ∀m. n ≠ m ⟶ P n ∩ P m = {}" 
  and  "∀n. (A ∩ (P n)) ≠ {}"
  shows "infinite (⋃n. (A ∩ (P n)))" 
proof-
  let ?f = "λx. SOME n. x∈(A ∩ (P n))"
  have "∀n. ∃x∈(⋃n. (A ∩ (P n))). n = ?f(x)"
  proof
    fix n
    obtain a where a:  "a ∈ (A ∩ (P n))" using assms(2) by auto
    {fix m
    have  "a ∈ (A ∩ (P m)) ⟶ m=n" 
    proof(rule impI)
      assume hip: "a ∈ A ∩ P m" show "m =n"
      proof(rule ccontr)
        assume "m ≠ n"
        hence "P m ∩ P n = {}" using assms(1) by auto
        thus False using a hip by auto
      qed
    qed}
    hence "⋀m. a ∈ A ∩ P m ⟹ m = n" by auto
    hence 1: "?f(a) = n"  using a  some_equality by auto
    have "a∈(⋃n. (A ∩ (P n)))" using a by auto
    thus "∃x∈⋃n. A ∩ P n. n = (SOME n. x ∈ A ∩ P n)" using 1 by auto
  qed
  hence  "∃f:: 'a ⇒  nat. ∀n. ∃x∈((⋃n. (A ∩ (P n)))). n = f(x)" 
    using exI  by auto
  thus ?thesis using surjective_infinite by auto
qed

lemma infinite_path:
  assumes  "infinite_tree A r" and  "finitely_branching A r"
  and  I: "∀F ∈ (ℱ A r). t_v_evaluation I F = Ttrue"
shows "infinite (ℬ A I)"
proof-
  have a: "∀n. ∀m.  n ≠ m ⟶ level A r n ∩ level A r m = {}"
    using uniqueness_level[of _ _ A r] by auto 
  have  "∀n. ℬ A I ∩ level A r n ≠ {}"
    using `infinite_tree A r`
          `finitely_branching A r` I  intersection_branch_set_nodes_at_level[of A r]
    by blast  
  hence  "infinite (⋃n. (ℬ A I) ∩  level A r n)"
    using family_intersection_infinita  a  by auto
  thus "infinite (ℬ A I)"by auto 
qed

theorem Koenig_Lemma:
  assumes  "infinite_tree (A::'nodes:: countable set) r" 
  and "finitely_branching A r" 
  shows  "∃B. infinite_path B A r"
proof-
  have  "satisfiable (𝒯 A r)" 
  proof- 
    have "∀ S. S ⊆ (𝒯 A r) ∧ (finite S) ⟶ satisfiable S" 
      using `infinite_tree A r` `finitely_branching A r` satisfiable_path
      by auto   
    thus "satisfiable (𝒯 A r)"
      using Compactness_Theorem[of "(𝒯 A r)"] by auto
  qed
  hence "∃I. (∀F ∈ (𝒯 A r). t_v_evaluation I F = Ttrue)" 
    by(unfold satisfiable_def, unfold model_def, auto) 
  then obtain I where I:  "∀F ∈ (𝒯 A r). t_v_evaluation I F = Ttrue"  
    by auto
  hence "∀F ∈ (ℱ A r) ∪ (𝒢 A r) ∪ (ℋ A r). t_v_evaluation I F = Ttrue"
    by(unfold 𝒯_def)
  hence I1:  "∀F ∈ (ℱ A r). t_v_evaluation I F = Ttrue" 
  and   I2:  "∀F ∈ (𝒢 A r). t_v_evaluation I F = Ttrue"
  and   I3:  "∀F ∈ (ℋ A r). t_v_evaluation I F = Ttrue" 
    by auto 
  let ?B = "(ℬ A I)"
  have "infinite_path ?B A r"
  proof(unfold infinite_path_def)
    show "path ?B A r ∧ infinite ?B" 
    proof(rule conjI)
      show "path ?B A r"
        using  `infinite_tree A r` `finitely_branching A r` I is_path[of A r]
        by auto   
      show "infinite (ℬ A I)"
        using `infinite_tree A r` `finitely_branching A r` I1 infinite_path
      by auto     
    qed
  qed
  thus "∃B. infinite_path B A r" by auto
qed
           
end