Syntax (Section 2.1)

inductive Formula : Type

• bottom : Formula
• atom_prop : ℕ → Formula
• neg : Formula → Formula
• and : Formula → Formula → Formula
• box : Program → Formula → Formula

instance instReprProgram : Repr Program

Equations

• instReprProgram = { reprPrec := reprProgram✝ }

instance instReprFormula : Repr Formula

Equations

• instReprFormula = { reprPrec := reprFormula✝ }

instance instDecidableEqProgram : DecidableEq Program

Equations

• instDecidableEqProgram = decEqProgram✝

instance instDecidableEqFormula : DecidableEq Formula

Equations

• instDecidableEqFormula = decEqFormula✝

inductive Program : Type

• atom_prog : ℕ → Program
• sequence : Program → Program → Program
• union : Program → Program → Program
• star : Program → Program
• test : Formula → Program

Abbreviations and Notation

def Formula.or : Formula → Formula → Formula

Equations

• x✝¹⋁x✝ = (~(~x✝¹)⋀(~x✝))

def Formula.boxes : List Program → Formula → Formula

□(αs,φ)

Equations

• (⌈⌈x✝¹⌉⌉x✝) = List.foldr (fun (β : Program) (φ : Formula) => ⌈β⌉φ) x✝ x✝¹

def Program.steps : List Program → Program

Equations

• Program.steps [] = (?'(~Formula.bottom))
• Program.steps (p :: ps) = (p;'Program.steps ps)

def «term·_» : Lean.ParserDescr

Equations

• «term·_» = Lean.ParserDescr.node `«term·_» 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "·") (Lean.ParserDescr.cat `term 70))

def «term·__1» : Lean.ParserDescr

Equations

• «term·__1» = Lean.ParserDescr.node `«term·__1» 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "·") (Lean.ParserDescr.cat `term 70))

def «term~_» : Lean.ParserDescr

Equations

• «term~_» = Lean.ParserDescr.node `«term~_» 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 11))

instance Formula.instBot : Bot Formula

Equations

• Formula.instBot = { bot := Formula.bottom }

instance Formula.insTop : Top Formula

Equations

• Formula.insTop = { top := ~Formula.bottom }

def «term_⋀_» : Lean.TrailingParserDescr

Equations

• «term_⋀_» = Lean.ParserDescr.trailingNode `«term_⋀_» 66 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋀") (Lean.ParserDescr.cat `term 66))

def «term_⋁_» : Lean.TrailingParserDescr

Equations

• «term_⋁_» = Lean.ParserDescr.trailingNode `«term_⋁_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋁") (Lean.ParserDescr.cat `term 60))

def «term_↣_» : Lean.TrailingParserDescr

Equations

• «term_↣_» = Lean.ParserDescr.trailingNode `«term_↣_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↣ ") (Lean.ParserDescr.cat `term 55))

def «term_⟷_» : Lean.TrailingParserDescr

Equations

• «term_⟷_» = Lean.ParserDescr.trailingNode `«term_⟷_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟷ ") (Lean.ParserDescr.cat `term 55))

def «term⌈_⌉_» : Lean.ParserDescr

Equations

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

def «term⌈⌈_⌉⌉_» : Lean.ParserDescr

Equations

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

def «term_;'_» : Lean.TrailingParserDescr

Equations

• «term_;'_» = Lean.ParserDescr.trailingNode `«term_;'_» 33 33 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ";'") (Lean.ParserDescr.cat `term 34))

def «term_⋓_» : Lean.TrailingParserDescr

Equations

• «term_⋓_» = Lean.ParserDescr.trailingNode `«term_⋓_» 33 33 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋓") (Lean.ParserDescr.cat `term 34))

def «term∗_» : Lean.ParserDescr

Equations

• «term∗_» = Lean.ParserDescr.node `«term∗_» 33 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∗") (Lean.ParserDescr.cat `term 33))

def term?'_ : Lean.ParserDescr

Equations

• term?'_ = Lean.ParserDescr.node `term?'_ 33 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "?'") (Lean.ParserDescr.cat `term 33))

def Program.isAtomic : Program → Prop

Equations

• (·a).isAtomic = (true = true)
• x✝.isAtomic = (false = true)

instance instDecidablePredProgramIsAtomic : DecidablePred Program.isAtomic

Equations

• instDecidablePredProgramIsAtomic (·a) = decidable_of_decidable_of_iff instDecidablePredProgramIsAtomic._proof_63
• instDecidablePredProgramIsAtomic (a;'a_1) = decidable_of_decidable_of_iff instDecidablePredProgramIsAtomic._proof_64
• instDecidablePredProgramIsAtomic (a⋓a_1) = decidable_of_decidable_of_iff instDecidablePredProgramIsAtomic._proof_64
• instDecidablePredProgramIsAtomic (∗a) = decidable_of_decidable_of_iff instDecidablePredProgramIsAtomic._proof_64
• instDecidablePredProgramIsAtomic (?'a) = decidable_of_decidable_of_iff instDecidablePredProgramIsAtomic._proof_64

theorem Program.isAtomic_iff {α : Program} : α.isAtomic ↔ ∃ (a : ℕ), α = ·a

def Program.isStar : Program → Prop

Equations

• (∗a).isStar = (true = true)
• x✝.isStar = (false = true)

instance instDecidablePredProgramIsStar : DecidablePred Program.isStar

Equations

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

theorem Program.isStar_iff {α : Program} : α.isStar ↔ ∃ (β : Program), α = (∗β)

@[simp]

theorem Formula.boxes_nil {φ : Formula} : (⌈⌈[]⌉⌉φ) = φ

@[simp]

theorem Formula.boxes_cons {β : Program} {δ : List Program} {φ : Formula} : (⌈⌈β :: δ⌉⌉φ) = ⌈β⌉⌈⌈δ⌉⌉φ

theorem boxes_last {δ : List Program} {α : Program} {φ : Formula} : (⌈⌈δ ++ [α]⌉⌉φ) = ⌈⌈δ⌉⌉⌈α⌉φ

theorem boxes_append {as bs : List Program} {P : Formula} : (⌈⌈as ++ bs⌉⌉P) = ⌈⌈as⌉⌉⌈⌈bs⌉⌉P

Loaded Formulas

inductive AnyFormula : Type

• normal : Formula → AnyFormula
• loaded : LoadFormula → AnyFormula

instance instReprAnyFormula : Repr AnyFormula

Equations

• instReprAnyFormula = { reprPrec := reprAnyFormula✝ }

instance instReprLoadFormula : Repr LoadFormula

Equations

• instReprLoadFormula = { reprPrec := reprLoadFormula✝ }

instance instDecidableEqAnyFormula : DecidableEq AnyFormula

Equations

• instDecidableEqAnyFormula = decEqAnyFormula✝

instance instDecidableEqLoadFormula : DecidableEq LoadFormula

Equations

• instDecidableEqLoadFormula = decEqLoadFormula✝

inductive LoadFormula : Type

• box : Program → AnyFormula → LoadFormula

instance instCoeFormulaAnyFormula : Coe Formula AnyFormula

Equations

• instCoeFormulaAnyFormula = { coe := AnyFormula.normal }

instance instCoeLoadFormulaAnyFormula : Coe LoadFormula AnyFormula

Equations

• instCoeLoadFormulaAnyFormula = { coe := AnyFormula.loaded }

inductive AnyNegFormula : Type

• neg : AnyFormula → AnyNegFormula

def loadMulti : List Program → Program → Formula → LoadFormula

Equations

• loadMulti x✝² x✝¹ x✝ = List.foldr (fun (β : Program) (lf : LoadFormula) => ⌊β⌋AnyFormula.loaded lf) (⌊x✝¹⌋AnyFormula.normal x✝) x✝²

@[simp]

theorem loadMulti_nil {α : Program} {φ : Formula} : loadMulti [] α φ = ⌊α⌋AnyFormula.normal φ

@[simp]

theorem loadMulti_cons {β : Program} {δ : List Program} {α : Program} {φ : Formula} : loadMulti (β :: δ) α φ = ⌊β⌋AnyFormula.loaded (loadMulti δ α φ)

def LoadFormula.boxes : List Program → LoadFormula → LoadFormula

Equations

• (⌊⌊x✝¹⌋⌋x✝) = List.foldr (fun (β : Program) (lf : LoadFormula) => ⌊β⌋AnyFormula.loaded lf) x✝ x✝¹

@[simp]

theorem LoadFormula.boxes_nil {χ : LoadFormula} : (⌊⌊[]⌋⌋χ) = χ

theorem LoadFormula.boxes_cons {b : Program} {bs : List Program} {φ : LoadFormula} : (⌊⌊b :: bs⌋⌋φ) = ⌊b⌋AnyFormula.loaded (⌊⌊bs⌋⌋φ)

def LoadFormula.unload : LoadFormula → Formula

Equations

• (⌊α⌋AnyFormula.normal φ).unload = ⌈α⌉φ
• (⌊α⌋AnyFormula.loaded χ).unload = ⌈α⌉χ.unload

@[simp]

theorem unload_loadMulti {δ : List Program} {α : Program} {φ : Formula} : (loadMulti δ α φ).unload = ⌈⌈δ⌉⌉⌈α⌉φ

inductive NegLoadFormula : Type

• neg : LoadFormula → NegLoadFormula

instance instReprNegLoadFormula : Repr NegLoadFormula

Equations

• instReprNegLoadFormula = { reprPrec := reprNegLoadFormula✝ }

instance instDecidableEqNegLoadFormula : DecidableEq NegLoadFormula

Equations

• instDecidableEqNegLoadFormula = decEqNegLoadFormula✝

def «term⌊_⌋_» : Lean.ParserDescr

Equations

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

def «term⌊⌊_⌋⌋_» : Lean.ParserDescr

Equations

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

def «term~'_» : Lean.ParserDescr

Equations

• «term~'_» = Lean.ParserDescr.node `«term~'_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~'") (Lean.ParserDescr.cat `term 0))

def «term~''_» : Lean.ParserDescr

Equations

• «term~''_» = Lean.ParserDescr.node `«term~''_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~''") (Lean.ParserDescr.cat `term 1023))

def negUnload : NegLoadFormula → Formula

Equations

• negUnload (~'a) = (~a.unload)

theorem loadBoxes_append {as bs : List Program} {P : LoadFormula} : (⌊⌊as ++ bs⌋⌋P) = ⌊⌊as⌋⌋⌊⌊bs⌋⌋P

theorem loadBoxes_last {a : Program} {as : List Program} {c : Program} {P : LoadFormula} : (~'⌊a⌋AnyFormula.loaded (⌊⌊as ++ [c]⌋⌋P)) = ~'⌊a⌋AnyFormula.loaded (⌊⌊as⌋⌋⌊c⌋AnyFormula.loaded P)

@[simp]

theorem unload_boxes {δ : List Program} {φ : LoadFormula} : (⌊⌊δ⌋⌋φ).unload = ⌈⌈δ⌉⌉φ.unload

@[simp]

theorem unload_neg_loaded {α : Program} {χ : LoadFormula} : (~'⌊α⌋AnyFormula.loaded χ).1.unload = ⌈α⌉χ.unload

@[simp]

theorem unload_neg_normal {α : Program} {φ : Formula} : (~'⌊α⌋AnyFormula.normal φ).1.unload = ⌈α⌉φ

def AnyFormula.loadBoxes : List Program → AnyFormula → AnyFormula

Load a possibly already loaded formula χ with a sequence δ of boxes. The result is loaded iff δ≠[] or χ was loaded.

Equations

• AnyFormula.loadBoxes x✝¹ x✝ = List.foldr (fun (β : Program) (lf : AnyFormula) => AnyFormula.loaded (⌊β⌋lf)) x✝ x✝¹

@[simp]

theorem AnyFormula.boxes_nil {ξ : AnyFormula} : loadBoxes [] ξ = ξ

@[simp]

theorem AnyFormula.loadBoxes_cons {α : Program} {γ : List Program} {ξ : AnyFormula} : loadBoxes (α :: γ) ξ = loaded (⌊α⌋loadBoxes γ ξ)

theorem AnyFormula.loadBoxes_append {as bs : List Program} {φ : AnyFormula} : loadBoxes (as ++ bs) φ = loadBoxes as (loadBoxes bs φ)

theorem AnyFormula.loadBoxes_loaded_eq_loaded_boxes {δ : List Program} {χ : LoadFormula} : loadBoxes δ (loaded χ) = loaded (⌊⌊δ⌋⌋χ)

def AnyFormula.unload : AnyFormula → Formula

Equations

• (AnyFormula.normal a).unload = a
• (AnyFormula.loaded a).unload = a.unload

theorem box_loadBoxes_append_eq_of_loaded_eq_loadBoxes {χ' : LoadFormula} {αs : List Program} {φ : Formula} {d : Program} {δ : List Program} (h : AnyFormula.loaded χ' = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (⌊d⌋AnyFormula.loadBoxes (δ ++ αs) (AnyFormula.normal φ)) = ⌊⌊d :: δ⌋⌋χ'

@[simp]

theorem AnyFormulaBoxBoxes_eq_FormulaBoxLoadBoxes_inside_unload {α : Program} {αs : List Program} {φ : Formula} : (⌊α⌋AnyFormula.loadBoxes αs (AnyFormula.normal φ)).unload = ⌈α⌉(AnyFormula.loadBoxes αs (AnyFormula.normal φ)).unload

theorem AnyFormula.loadBoxes_unload_eq_boxes {βs : List Program} {φ : Formula} : (loadBoxes βs (normal φ)).unload = ⌈⌈βs⌉⌉φ

theorem loaded_eq_to_unload_eq (χ : LoadFormula) (αs : List Program) (φ : Formula) (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : χ.unload = ⌈⌈αs⌉⌉φ

Spliting of loaded formulas

def AnyFormula.split (af : AnyFormula) : List Program × Formula

Split any formula into the list of loaded boxes and the free formula.

Equations

• (AnyFormula.loaded lf).split = lf.split
• (AnyFormula.normal f).split = ([], f)

def LoadFormula.split (lf : LoadFormula) : List Program × Formula

Split a loaded formula into the list of loaded boxes and the free formula.

Equations

• (⌊a⌋a_1).split = (fun (x : List Program × Formula) => match x with | (δ, f) => (a :: δ, f)) a_1.split

@[simp]

theorem AnyFormula.split_normal (φ : Formula) : (normal φ).split = ([], φ)

theorem AnyFormula.box_split {α : Program} (af : AnyFormula) : (⌊α⌋af).split = (α :: af.split.fst, af.split.snd)

@[simp]

theorem LoadFormula.split_list_not_empty (lf : LoadFormula) : lf.split.fst ≠ []

def loadMulti_nonEmpty (δ : List Program) (h : δ ≠ []) : Formula → LoadFormula

Equations

• loadMulti_nonEmpty [] h x✝ = ⋯.elim
• loadMulti_nonEmpty [α] x_3 x✝ = ⌊α⌋AnyFormula.normal x✝
• loadMulti_nonEmpty (α :: d :: δ) x_3 x✝ = ⌊α⌋AnyFormula.loaded (loadMulti_nonEmpty (d :: δ) ⋯ x✝)

@[simp]

theorem loadMulti_nonEmpty_box {δ : List Program} {α : Program} {h' : α :: δ ≠ []} {φ : Formula} (h : δ ≠ []) : loadMulti_nonEmpty (α :: δ) h' φ = ⌊α⌋AnyFormula.loaded (loadMulti_nonEmpty δ h φ)

theorem LoadFormula.split_eq_loadMulti_nonEmpty {δ : List Program} {φ : Formula} (lf : LoadFormula) (h : lf.split = (δ, φ)) : lf = loadMulti_nonEmpty δ ⋯ φ

theorem LoadFormula.split_eq_loadMulti_nonEmpty' {δ : List Program} {φ : Formula} (lf : LoadFormula) (h : δ ≠ []) (h2 : lf.split = (δ, φ)) : lf = loadMulti_nonEmpty δ h φ

theorem loadMulti_nonEmpty_eq_loadMulti {δ : List Program} {α : Program} {h : δ ++ [α] ≠ []} {φ : Formula} : loadMulti_nonEmpty (δ ++ [α]) h φ = loadMulti δ α φ

theorem LoadFormula.split_eq_loadMulti (lf : LoadFormula) {δ : List Program} {α : Program} {φ : Formula} (h : lf.split = (δ ++ [α], φ)) : lf = loadMulti δ α φ

theorem LoadFormula.exists_splitLast (lf : LoadFormula) : ∃ (δ : List Program), ∃ (α : Program), lf.split.fst = δ ++ [α]

theorem LoadFormula.exists_loadMulti (lf : LoadFormula) : ∃ (δ : List Program), ∃ (α : Program), ∃ (φ : Formula), lf = loadMulti δ α φ

theorem loadMulti_eq_of_some {d : Program} {δ : List Program} {β : Program} {φ : Formula} (h : δ.head? = some d) : loadMulti δ β φ = ⌊d⌋AnyFormula.loaded (loadMulti δ.tail β φ)

theorem loadMulti_eq_loadBoxes {δ : List Program} {α : Program} {φ : Formula} : AnyFormula.loaded (loadMulti δ α φ) = AnyFormula.loadBoxes (δ ++ [α]) (AnyFormula.normal φ)