Documentation

Pdl.TableauPath

Navigating through tableaux with PathIn #

To define relations between nodes in a tableau we need to represent the whole tableau and point to a specific node inside it. This is the PathIn type. Its values say "go to this child, then to this child, ... stop here."

inductive PathIn {Hist : History} {X : Sequent} :
Tableau Hist XType

A path in a tableau. Three constructors for the empty path, a local step or a pdl step. The loc and pdl steps correspond to two out of three constructors of Tableau. A PathIn only goes downwards, it cannot use LoadedPathRepeats.

Instances For
    instance instDecidableEqPathIn {Hist✝ : History} {X✝ : Sequent} {a✝ : Tableau Hist✝ X✝} :
    Equations
    def instDecidableEqPathIn.decEq {Hist✝ : History} {X✝ : Sequent} {a✝ : Tableau Hist✝ X✝} (x✝ x✝¹ : PathIn a✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      def tabAt {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :
      PathIn tab(H : History) × (X : Sequent) × Tableau H X
      Equations
      Instances For
        def PathIn.append {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) :
        PathIn tab
        Equations
        Instances For
          @[simp]
          theorem append_eq_iff_eq {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (s : PathIn tab) (p q : PathIn (tabAt s).snd.snd) :
          s.append p = s.append q p = q
          @[simp]
          theorem PathIn.eq_append_iff_other_eq_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) :
          p = p.append q q = nil
          theorem PathIn.nil_eq_append_iff_both_eq_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) :
          nil = p.append q p = nil q = nil
          @[simp]
          theorem tabAt_append {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) :
          @[simp]
          theorem tabAt_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} :
          @[simp]
          theorem tabAt_loc {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y endNodesOf ltTableau (X✝ :: Hist✝) Y} {a✝ : Sequent} {Y_in : a✝ endNodesOf lt} {tail : PathIn (next a✝ Y_in)} :
          tabAt (PathIn.loc Y_in tail) = tabAt tail
          @[simp]
          theorem tabAt_pdl {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {bas : X✝.basic} {Y✝ : Sequent} {r : PdlRule X✝ Y✝} {next : Tableau (X✝ :: Hist✝) Y✝} {tail : PathIn next} :
          tabAt tail.pdl = tabAt tail
          def nodeAt {H : History} {X : Sequent} {tab : Tableau H X} (p : PathIn tab) :

          Given a path to node t, this is its label Λ(t).

          Equations
          Instances For
            @[simp]
            theorem nodeAt_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} :
            @[simp]
            theorem nodeAt_loc {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y endNodesOf ltTableau (X✝ :: Hist✝) Y} {a✝ : Sequent} {Y_in : a✝ endNodesOf lt} {tail : PathIn (next a✝ Y_in)} :
            nodeAt (PathIn.loc Y_in tail) = nodeAt tail
            @[simp]
            theorem nodeAt_pdl {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {bas : X✝.basic} {Y✝ : Sequent} {r : PdlRule X✝ Y✝} {next : Tableau (X✝ :: Hist✝) Y✝} {tail : PathIn next} :
            nodeAt tail.pdl = nodeAt tail
            @[simp]
            theorem nodeAt_append {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) :
            def PathIn.head {Hist : History} {X : Sequent} {tab : Tableau Hist X} :
            PathIn tabSequent
            Equations
            Instances For
              def PathIn.last {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) :
              Equations
              Instances For
                def PathIn.length {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) :

                The length of a path is the number of actual steps.

                Equations
                Instances For
                  theorem append_length {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {p : PathIn tab} (q : PathIn (tabAt p).snd.snd) :

                  Edge Relation #

                  def edge {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (s t : PathIn tab) :

                  Relation s ⋖_ t says t is a child of s. Two cases, both defined via append.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Notation ⋖_ for edge (because ⋖ is taken in Mathlib).

                    Equations
                    Instances For
                      theorem edge_append_loc_nil {sX : Sequent} {sHist : List Sequent} {nrep : ¬rep sHist sX} {nbas : ¬sX.basic} {X : History} {Hist : Sequent} {tab : Tableau X Hist} (s : PathIn tab) {lt : LocalTableau sX} (next : (Y : Sequent) → Y endNodesOf ltTableau (sX :: sHist) Y) {Y : Sequent} (Y_in : Y endNodesOf lt) (tabAt_s_def : tabAt s = sHist, sX, Tableau.loc nrep nbas lt next) :

                      Appending a one-step loc path is also a ⋖_ child. When using this, this may be helpful: convert this; rw [← heq_iff_eq, heq_eqRec_iff_heq, eqRec_heq_iff_heq].

                      @[simp]
                      theorem edge_append_pdl_nil {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {s : PathIn a✝²} {nrep : ¬rep (tabAt s).fst (tabAt s).snd.fst} {bas : (tabAt s).snd.fst.basic} {Y✝ : Sequent} {r : PdlRule (tabAt s).snd.fst Y✝} {next : Tableau ((tabAt s).snd.fst :: (tabAt s).fst) Y✝} (h : (tabAt s).snd.snd = Tableau.pdl nrep bas r next) :

                      Appending a one-step pdl path is also a ⋖_ child.

                      @[simp]
                      theorem nil_edge_loc_nil {X Y : Sequent} {Hist : List Sequent} {nrep : ¬rep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {Y_in : Y endNodesOf lt} {next : (Y : Sequent) → Y endNodesOf ltTableau (X :: Hist) Y} :
                      @[simp]
                      theorem nil_edge_pdl_nil {Hist : List Sequent} {X : Sequent} {nrep : ¬rep Hist X} {bas : X.basic} {Y : Sequent} {r : PdlRule X Y} {next : Tableau (X :: Hist) Y} :
                      @[simp]
                      theorem loc_edge_loc_iff_edge {Y X : Sequent} {lt : LocalTableau X} {Y_in : Y endNodesOf lt} {tail : List Sequent} {next : (Y : Sequent) → Y endNodesOf ltTableau (X :: tail) Y} {nrep : ¬rep tail X} {nbas : ¬X.basic} {t s : PathIn (next Y Y_in)} :
                      (PathIn.loc Y_in t) ⋖_ (PathIn.loc Y_in s) t ⋖_ s
                      @[simp]
                      theorem pdl_edge_pdl_iff_edge {X Y : Sequent} {r : PdlRule X Y} {tail : List Sequent} {next : Tableau (X :: tail) Y} {nrep : ¬rep tail X} {bas : X.basic} {t s : PathIn next} :
                      t.pdl ⋖_ s.pdl t ⋖_ s
                      theorem not_edge_nil {Hist : History} {X : Sequent} (tab : Tableau Hist X) (t : PathIn tab) :

                      The root has no parent. Note this holds even when Hist ≠ [].

                      theorem nodeAt_loc_nil {X Y : Sequent} {H : List Sequent} {lt : LocalTableau X} {nrep : ¬rep H X} {nbas : ¬X.basic} (next : (Y : Sequent) → Y endNodesOf ltTableau (X :: H) Y) (Y_in : Y endNodesOf lt) :
                      theorem nodeAt_pdl_nil {X : Sequent} {Hist : List Sequent} {Y : Sequent} {nrep : ¬rep Hist X} {bas : X.basic} (child : Tableau (X :: Hist) Y) (r : PdlRule X Y) :
                      theorem length_succ_eq_length_of_edge {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} :
                      s ⋖_ ts.length + 1 = t.length

                      The length of edge-related paths differs by one.

                      theorem edge_then_length_lt {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} (s_t : s ⋖_ t) :
                      def edge_natLT_relHom {Hist : History} {X : Sequent} {tab : Tableau Hist X} :
                      Equations
                      Instances For
                        theorem edge.wellFounded {Hist : History} {X : Sequent} {tab : Tableau Hist X} :

                        The ⋖_ relation in a tableau is well-founded. Proven by lifting the relation to the length of histories. That length goes up with ⋖_, so because < is wellfounded on Nat also ⋖_ is well-founded via RelHomClass.wellFounded.

                        instance edge.isAsymm {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :
                        instance instLTPathIn {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :
                        LT (PathIn tab)

                        Enable "<" notation for transitive closure of ⋖_.

                        Equations
                        instance instLEPathIn {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :
                        LE (PathIn tab)

                        Enable "≤" notation for reflexive transitive closure of ⋖_

                        Equations
                        instance edge.TransGen_isAsymm {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :

                        The "<" in a tableau is antisymmetric.

                        theorem not_path_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} :
                        theorem edge_is_strict_ordering {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} :
                        s ⋖_ ts t
                        theorem path_is_strict_ordering {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} :
                        s < ts t
                        theorem PathIn.init_inductionOn {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) {motive : PathIn tabProp} (root : motive nil) (step : ∀ (t : PathIn tab), motive t∀ {s : PathIn tab}, t ⋖_ smotive s) :
                        motive t

                        An induction principle for PathIn with a base case at the root of the tableau and an induction step using the edge relation ⋖_.

                        QUESTIONS:

                        • Do we need to add any of these attributes? @[induction_eliminator, elab_as_elim]
                        • Should it be a def or a theorem? (motive to Prop or to Sort u?)
                        theorem PathIn.nil_le_anything {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {t : PathIn a✝²} :
                        theorem PathIn.loc_le_loc_of_le {Hist : History} {X : Sequent} {Y : ¬rep Hist X} {nrep : ¬X.basic} {nbas : LocalTableau X} {lt : (Y : Sequent) → Y endNodesOf nbasTableau (X :: Hist) Y} {next : Sequent} {Z_in : next endNodesOf nbas} {t1 t2 : PathIn (lt next Z_in)} (h : t1 t2) :
                        loc Z_in t1 loc Z_in t2
                        theorem PathIn.pdl_le_pdl_of_le {Hist : History} {X Y : Sequent} {nrep : ¬rep Hist X} {bas : X.basic} {r : PdlRule X Y} {Z_in : Tableau (X :: Hist) Y} {t1 t2 : PathIn Z_in} (h : t1 t2) :
                        t1.pdl t2.pdl

                        From Path to History #

                        def PathIn.toHistory {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) :

                        Convert a path to a History. Does not include the last node. The history of .nil is [] because this will not go into Hist.

                        Equations
                        Instances For
                          def PathIn.toList {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) :

                          Convert a path to a list of nodes. Reverse of the history and does include the last node. The list of .nil is [X].

                          Equations
                          Instances For
                            theorem PathIn.toHistory_eq_Hist {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) :
                            t.toHistory ++ Hist = (tabAt t).fst

                            A path gives the same list of nodes as the history of its last node.

                            @[simp]
                            theorem PathIn.loc_length_eq {X Y : Sequent} {Hist : List Sequent} {nrep : ¬rep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y endNodesOf ltTableau (X :: Hist) Y} (Y_in : Y endNodesOf lt) (tail : PathIn (next Y Y_in)) :
                            @[simp]
                            theorem PathIn.pdl_length_eq {X Y : Sequent} {Hist : List Sequent} {nrep : ¬rep Hist X} {bas : X.basic} {next : Tableau (X :: Hist) Y} {r : PdlRule X Y} (tail : PathIn next) :
                            def PathIn.prefix {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (t.length + 1)) :
                            PathIn tab

                            Prefix of a path, taking only the first k steps.

                            Equations
                            Instances For
                              theorem PathIn.prefix_toList_eq_toList_take {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (t.length + 1)) :
                              (t.prefix k).toList = List.take (k + 1) t.toList

                              The list of a prefix of a path is the same as the prefix of the list of the path.

                              Path Rewinding #

                              def PathIn.rewind {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) :
                              PathIn tab

                              Rewinding a path, removing the last k steps. Cannot go into Hist. Used to go to the companion of a repeat. Returns .nil when k is the length of the whole path. We use +1 in the type because rewind 0 is always possible, even with history []. Defined using Fin.lastCases.

                              Hint: when proving stuff about rewind k, avoid induction on k, because rewind does not decrease k.

                              Equations
                              Instances For
                                theorem PathIn.rewind_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} {p : PathIn tab} :
                                p.rewind 0 = p

                                Rewinding 0 steps does nothing.

                                theorem PathIn.rewind_le {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) :
                                t.rewind k t
                                theorem PathIn.rewind_length_lt_length_of_gt_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) (k_gt_zero : k > 0) :

                                If we rewind by k > 0 steps then the length goes down.

                                theorem PathIn.rewind_lt_of_gt_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) (k_gt_zero : k > 0) :
                                t.rewind k < t
                                theorem PathIn.nodeAt_rewind_eq_toHistory_get {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) :

                                The node we get from rewinding k steps is element k+1 in the history.

                                theorem nil_iff_length_zero {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} :
                                theorem PathIn.loc_injective {Hist : History} {X : Sequent} {nrep : ¬rep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y endNodesOf ltTableau (X :: Hist) Y} {Y : Sequent} {Y_in : Y endNodesOf lt} {ta tb : PathIn (next Y Y_in)} :
                                loc Y_in ta = loc Y_in tbta = tb
                                theorem PathIn.pdl_injective {Hist : History} {X Y : Sequent} {nrep : ¬rep Hist X} {bas : X.basic} {next : Tableau (X :: Hist) Y} (r : PdlRule X Y) (ta tb : PathIn next) :
                                ta.pdl = tb.pdlta = tb
                                theorem edge_is_irreflexive {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} :
                                ¬a ⋖_ a
                                theorem path_then_length_lt {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} (s_t : s < t) :
                                theorem path_is_irreflexive {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} :
                                theorem rewind_order_reversing {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h : k < k') :
                                t.rewind k' t.rewind k
                                theorem PathIn.loc_lt_loc_of_lt {Hist : History} {X : Sequent} {Y : ¬rep Hist X} {nrep : ¬X.basic} {nbas : LocalTableau X} {lt : (Y : Sequent) → Y endNodesOf nbasTableau (X :: Hist) Y} {next : Sequent} {Z_in : next endNodesOf nbas} {t1 t2 : PathIn (lt next Z_in)} (h : t1 < t2) :
                                loc Z_in t1 < loc Z_in t2
                                theorem PathIn.pdl_lt_pdl_of_lt {Hist : History} {X Y : Sequent} {nrep : ¬rep Hist X} {bas : X.basic} {r : PdlRule X Y} {Z_in : Tableau (X :: Hist) Y} {t1 t2 : PathIn Z_in} (h : t1 < t2) :
                                t1.pdl < t2.pdl
                                theorem one_is_one_helper {k : } {h : k > 0} :
                                1 = 1
                                theorem rewind_of_edge_is_eq {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} (a_b : a ⋖_ b) :
                                b.rewind 1 = a
                                theorem rewind_order_reversing_if_not_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h : k < k') (h' : t PathIn.nil) :
                                t.rewind k' < t.rewind k
                                theorem rewind_is_inj {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h1 : t.rewind k = t.rewind k') :
                                k = k'
                                theorem one_is_one_rewind_helper {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {b : PathIn tab} {k : Fin (List.length b.toHistory + 1)} (h : (b.rewind k) ⋖_ b) :
                                k = 1
                                theorem edge_leftInjective {Hist : History} {X : Sequent} {tab : Tableau Hist X} (a b c : PathIn tab) :
                                a ⋖_ cb ⋖_ ca = b
                                theorem edge_revEuclideanHelper {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (a b c : PathIn tab) :
                                a ⋖_ cb < cb a
                                theorem path_revEuclidean {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (a b c : PathIn tab) :
                                a < cb < ca < b b < a b = a
                                theorem path_revEuclidean' {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (a b c : PathIn tab) :
                                a < cb < ca b b a
                                theorem edge_inc_length_by_one {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} (a_b : a ⋖_ b) :
                                theorem rewind_helper {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} {k : Fin (List.length a.toHistory + 1)} (a_b : a ⋖_ b) :
                                b.rewind (Fin.cast k.succ) = a.rewind k
                                theorem exists_rewind_of_le {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} (h : a b) :
                                ∃ (k : Fin (List.length b.toHistory + 1)), b.rewind k = a
                                theorem exists_rewinds_middle {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b c : PathIn tab} (h : a b) (h' : b c) :
                                ∃ (k : Fin (List.length c.toHistory + 1)) (k' : Fin (List.length c.toHistory + 1)), c.rewind k = a c.rewind k' = b k' k
                                def Finset.join {α : Type u_1} [DecidableEq α] (M : Finset (Finset α)) :

                                Finiteness and Wellfoundedness - #

                                Equations
                                Instances For
                                  def allPaths {Hist : History} {X : Sequent} (tab : Tableau Hist X) :
                                  Equations
                                  Instances For
                                    theorem allPaths_loc_cases {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y endNodesOf ltTableau (X✝ :: Hist✝) Y} (s : PathIn (Tableau.loc nrep nbas lt next)) :
                                    s allPaths (Tableau.loc nrep nbas lt next) s = PathIn.nil ∃ (Y : Sequent) (Y_in : Y endNodesOf lt) (t : { x : PathIn (next Y Y_in) // x allPaths (next Y Y_in) }), s = PathIn.loc Y_in t
                                    theorem PathIn.elem_allPaths {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) :
                                    instance PathIn.instFintype {Hist : History} {X : Sequent} {tab : Tableau Hist X} :

                                    A Tableau is finite. Should be useful to get converse well-foundedness of edge

                                    Equations
                                    theorem Finite.wellfounded_of_irrefl_TC {α : Type} [Finite α] (r : ααProp) (h : IsIrrefl α (Relation.TransGen r)) :
                                    theorem nodeAt_mem_History_of_edge {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} :
                                    p ⋖_ qnodeAt p (tabAt q).fst
                                    theorem mem_History_of_edge {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} {x : Sequent} :
                                    p ⋖_ qx (tabAt p).fstx (tabAt q).fst
                                    theorem mem_History_append {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p : PathIn a✝²} {X : Sequent} {q : PathIn (tabAt p).snd.snd} :
                                    X (tabAt p).fstX (tabAt (p.append q)).fst
                                    theorem edge_TransGen_then_mem_History {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} :
                                    theorem PathIn.mem_history_multisetEqTo_then_lrep {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) :
                                    (∃ Y(tabAt p).fst, Y.multisetEqTo (nodeAt p))(tabAt p).snd.snd.isLrep
                                    theorem single_of_transgen {α : Sort u_1} {r : ααProp} {a c : α} :
                                    Relation.TransGen r a c∃ (b : α), r a b
                                    instance flipEdge.instIsIrrefl {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :
                                    theorem flipEdge.wellFounded {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} :

                                    The flip edge relation in a tableau is well-founded.

                                    theorem PathIn.edge_upwards_inductionOn {Hist : History} {X : Sequent} {tab : Tableau Hist X} {motive : PathIn tabProp} (up : ∀ {u : PathIn tab}, (∀ {s : PathIn tab}, u ⋖_ smotive s)motive u) (t : PathIn tab) :
                                    motive t

                                    Induction principle going from the leaves (= childless nodes) to the root. Suppose whenever the motive holds at all children then it holds at the parent. Then it holds at all nodes.