You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
def liftPropToPurePred (σ p : Expr) : MetaM Expr := do
  trace[lentil.debug] "p is {p}"
  if ← Meta.isProp p then
    trace[lentil.debug] "lifted"
    
    if p.isTrue then
      mkAppOptM ``TLA.tla_true #[some σ]
    else if p.isFalse then
      mkAppOptM ``TLA.tla_false #[some σ]
    else
      mkAppOptM ``TLA.pure_pred #[some σ, some p]
  else
    pure p

partial def convertPropToTLAPredAux (alist : AssocList Expr Expr) (σ p : Expr) : MetaM Expr := do
  match_expr p with
  | And a b => do
    trace[lentil.debug] "And case: {a} and {b}"
    let a' ← go a ; let b' ← go b
    mkAppM ``TLA.tla_and #[a', b']
  | Or a b => do
    trace[lentil.debug] "Or case: {a} or {b}"
    let a' ← go a ; let b' ← go b
    mkAppM ``TLA.tla_or #[a', b']
  | Not a => do
    trace[lentil.debug] "Not case: not {a}"
    let a' ← go a
    mkAppM ``TLA.tla_not #[a']
  | Exists _ f => do
    trace[lentil.debug] "Exists case: ∃ {f}"
    
    let f ← whnfD f
    match f with
    | Expr.lam na a b bi =>
      let a' ← go a
      withLocalDecl na bi a' fun avar => do
        let b_ := b.instantiate1 avar
        let b' ← go b_
        let b'' ← mkLambdaFVars #[avar] b'
        mkAppM ``TLA.tla_exists #[b'']
    | _ =>
      let f' ← go f
      mkAppM ``TLA.tla_exists #[f']
  | _ =>
    
    match p with
    | Expr.forallE na a b bi =>
      
      if p.isArrow then
        trace[lentil.debug] "Arrow case: {a} → {b}"
        let a' ← go a ; let b' ← go b
        mkAppM ``TLA.tla_implies #[a', b']
      else
        trace[lentil.debug] "Forall case: ∀ {a}, {b}"
        
        let a' ← go a
        withLocalDecl na bi a' fun avar => do
          let b_ := b.instantiate1 avar
          let b' ← go b_
          let b'' ← mkLambdaFVars #[avar] b'
          mkAppM ``TLA.tla_forall #[b'']
    | _ =>
      
      trace[lentil.debug] "Terminal case: {p}"
      pure <| p.replace alist.find?
where go (p : Expr) : MetaM Expr :=
  convertPropToTLAPredAux alist σ p >>= liftPropToPurePred σ

partial def convertPropToTLAPred (alist : AssocList Expr Expr) (σ p : Expr) : MetaM Expr :=
  convertPropToTLAPredAux alist σ p >>= liftPropToPurePred σ

inductive LiftingCase where
   
  | Iff
   
  | Other
deriving Inhabited

instance : ToString LiftingCase where
  toString
    | LiftingCase.Iff => "Iff"
    | LiftingCase.Other => "Other"

private def guessWhereToStartAux (es xs : List Expr) : MetaM Nat :=
  match xs with
  | [] => pure 0
  | x :: xs' => if es.any x.occurs then pure xs.length else do
    
    let ty ← inferType x
    if (← getLevel ty).isZero then guessWhereToStartAux (ty :: es) xs' else pure xs.length

private def guessWhereToStart (thmStmt : Expr) : MetaM Nat := do
  forallTelescope thmStmt fun xs body =>
    guessWhereToStartAux [body] xs.reverse.toList

partial def convertTheoremStatement (thmStmt : Expr) (uName : Name) : MetaM (LiftingCase × Expr) := do
  
  let u := mkLevelSucc <| mkLevelParam uName
  
  withLocalDecl `σ BinderInfo.implicit (.sort u) fun σ => do
    let pred ← mkAppM ``TLA.pred #[σ]
    let n ← guessWhereToStart thmStmt
    forallBoundedTelescope thmStmt n fun xs body => do
      trace[lentil.debug] "xs := {xs}, body := {body}"
       
       
      let (_, xs') ← xs.foldlM (fun (xspre, xs'_) x => do
        let ty ← inferType x
        
        if [``Decidable, ``DecidableEq, ``DecidablePred].any ty.getAppFn'.isConstOf then
          pure (xspre.push x, xs'_)
        else
          let fv := x.fvarId!
          let n ← fv.getUserName
          let bi ← fv.getBinderInfo
          let ty' ← do
            if ← Meta.isProp ty then
              pure ty
            else
              
              trace[lentil.debug] "ty := {ty}"
              let res := ty.replace fun e => if e == .sort .zero then some pred else none
              trace[lentil.debug] "ty after replacement := {res}"
              pure res
          let ty' (yspre : Array Expr) := do pure <| ty'.replaceFVars xspre yspre
          pure (xspre.push x, xs'_.push (x, n, bi, ty'))) (#[], #[])
       
      withLocalDecls (xs'.map Prod.snd) fun ys => do
        let alist := xs'.zipWith (fun (x, _) y => (x, y)) ys
        let alist := alist.toList.toAssocList'
        match_expr body with
        | Iff a b => do
          trace[lentil.debug] "a := {a}, b := {b}"
          let a' ← convertPropToTLAPred alist σ a
          let b' ← convertPropToTLAPred alist σ b
          trace[lentil.debug] "a' := {a'}, b' := {b'}"
          
          let thmStmt' ← mkAppM ``Eq #[a', b'] >>= mkForallFVars (Array.append #[σ] ys)
          pure (LiftingCase.Iff, thmStmt')
        | _ =>
          let body' ← convertPropToTLAPred alist σ body
          let thmStmt' ← mkAppM ``TLA.valid #[body'] >>= mkForallFVars (Array.append #[σ] ys)
          pure (LiftingCase.Other, thmStmt')

partial def liftTheorem (thmName : Name) (liftedThmName : Option Name) : MetaM Unit := do
  let info ← getConstInfo thmName
  let ty := info.type
  let lvlParams := info.levelParams
  trace[lentil.debug] "to-be-lifted theorem statement : {ty}"
  
  let uName := mkUnusedName lvlParams `u
  let (lcase, ty') ← convertTheoremStatement ty uName
  trace[lentil.debug] "after conversion : {ty'}, case: {lcase}"
  if ty'.hasFVar || ty'.hasExprMVar then
    throwError "internal error: the converted result contains free variables or metavariables"
  
   
  let newThmName := liftedThmName.getD <| thmName.updatePrefix `TLA
  let noncomputable? := isNoncomputable (← getEnv) thmName
  let e ← mkIdent <$> mkFreshUserName `e
  let finalTac ← `(tactic| open Classical in (try solve
    | apply $(mkIdent <| `_root_ ++ thmName)
    | apply $(mkIdent thmName) ))   
  match lcase with
  | LiftingCase.Iff =>
    simpleProveTheorem newThmName (uName :: lvlParams) ty'
      (← `(term| by admit /- proof elided -/
      )) noncomputable?
  | LiftingCase.Other =>
    simpleProveTheorem newThmName (uName :: lvlParams) ty'
      (← `(term| by admit /- proof elided -/
      )) noncomputable?

elab "#tla_lift" idts:ident+ : command => Command.liftTermElabM do
  for idt in idts do
    
    let nm := idt.getId
    addTermInfo' idt (← Lean.mkConstWithLevelParams nm)
    TLA.Lifting.liftTheorem nm none

elab "#tla_lift" idt:ident "=>" nm:ident : command => Command.liftTermElabM do
  addTermInfo' idt (← Lean.mkConstWithLevelParams idt.getId)
  TLA.Lifting.liftTheorem idt.getId <| some nm.getId
  addTermInfo' nm (← Lean.mkConstWithLevelParams nm.getId)

def binderIdentToFunBinder (stx : TSyntax ``binderIdent) : MacroM (TSyntax ``Parser.Term.funBinder) :=
  match stx with
  | `(binderIdent| $x:ident) =>  `(Parser.Term.funBinder| $x:ident )
  | `(binderIdent| _ ) =>  `(Parser.Term.funBinder| _ )
  | _ => Macro.throwUnsupported

def simpleAddTheorem (name : Name) (lvlParams : List Name) (type value : Expr) (nonComputable? : Bool) : CoreM Unit := do
  let thm := Declaration.thmDecl <| mkTheoremValEx name lvlParams type value []
  if nonComputable? then
    addDecl <| thm
    setEnv <| addNoncomputable (← getEnv) name
  else
    addAndCompile thm

def simpleProveTheorem (name : Name) (lvlParams : List Name) (type : Expr) (proofScript : TSyntax `term)
    (nonComputable? : Bool) : MetaM Unit := do
  let proof ← liftCommandElabM <| Command.liftTermElabM do
    
    let proof ← Term.elabTermAndSynthesize proofScript type
    if proof.hasSorry then
      trace[lentil.debug] "theorem {name} : {type} := {proofScript}"
    
    
    check proof
    instantiateMVars proof
  simpleAddTheorem name lvlParams type proof nonComputable?

partial def mkUnusedName (names : List Name) (baseName : Name) : Name :=
  if not (names.contains baseName) then
    baseName
  else
    let rec loop (i : Nat := 0) : Name :=
      let w := Name.appendIndexAfter baseName i
      if names.contains w then
        loop (i + 1)
      else
        w
    loop 1

partial def generalizeExecStatesAuxFinder (e typ : Expr) (visited : List Expr) : List Expr :=
  match typ.find? (fun e' => match e' with
    | .app e1 e2 => e1 == e && !e2.hasLooseBVars && !(visited.contains e2)
    | _ => false) with
  | some res => generalizeExecStatesAuxFinder e typ (res.appArg! :: visited)  
  | none => visited.map (mkApp e)

partial def generalizeExecStatesAux (e typ : Expr) (mv : MVarId) : MetaM MVarId := do
  let targets := generalizeExecStatesAuxFinder e typ []
  if targets.isEmpty then return mv
  mv.withContext do
    
    
    let ss ← Array.range targets.length |>.mapM fun x => do mkFreshUserName <| Name.mkSimple <| "s" ++ ⟨List.replicate x '\''⟩
    let args : Array GeneralizeArg := ss.zip targets.toArray |>.map fun (s, expr) => { expr, xName? := s }
    let hyps := ((← getLocalHyps).map (·.fvarId!))
    let (_, _, mv') ← mv.generalizeHyp args hyps
    pure mv'

partial def generalizeExecStates (e : Expr) : TacticM Unit := withMainContext do
  
  let g ← getMainTarget >>= instantiateMVars
  let mv' ← generalizeExecStatesAux e g (← getMainGoal)
  replaceMainGoal [mv']
  
  withMainContext do
  let hyps ← getLCtx
  for hyp in hyps do
    if !hyp.isImplementationDetail then
      let mv' ← generalizeExecStatesAux e hyp.type (← getMainGoal)
      replaceMainGoal [mv']

partial def elabSimpFiniteExecTLAGoal : TacticM Unit := do
  withMainContext do
    evalTactic $ ← `(tactic| try simp [exec.satisfies] at * )
  withMainContext do
  let g ← getMainTarget >>= instantiateMVars
  let g := g.cleanupAnnotations
  if !g.isApp then throwError "the goal should be an application"
  let e := g.appArg!
  let k ← mkIdent <$> mkFreshUserName `k
  
  
  evalTactic $ ← `(tactic| tla_unfold_simp' ; (try simp at *) ; intro $k:ident )
  
  
  withMainContext do
  let hyps ← getLCtx
  for hyp in hyps do
    if !hyp.isImplementationDetail then forallTelescope hyp.type fun xs body => do
      
      if xs.size >= 1 then
        let x := xs[0]! |>.fvarId!
        if (← isDefEq (mkConst ``Nat) (← inferType xs[0]!)) then
          
          if body.find? (fun e' => match e' with
            | .app e1 e2 => e1 == e && e2.containsFVar x
            | _ => false) |>.isSome then
            evalTactic $ ← `(tactic| specialize $(mkIdent hyp.userName) $k:ident )
  
  
  
  withMainContext do
    evalTactic $ ← `(tactic| (repeat rw [← $(mkIdent ``Nat.add_comm) $k] at *) )
  
  generalizeExecStates e
  
  
  
  withMainContext do
    if e.occurs (← getMainTarget) then
      throwTacticEx `simp_finite_exec_goal (← getMainGoal)
  
  liftMetaTactic1 fun mv => do
    let mut toClear : Array FVarId := #[]
    for decl in ← getLCtx do
      if e.occurs decl.type then
        toClear := toClear.push decl.fvarId
    mv.tryClearMany toClear

def make_conjunction_of_holes (headingop : TSyntax `tlafml_heading_op) (n : Nat) : MacroM (TSyntax `tlafml) := do
  let q : TSyntax `term ← `(term|_)
  match n with
  | 0 => Macro.throwUnsupported
  | 1 => do
    `(tlafml| ($headingop:tlafml_heading_op ($q:term)) )
  | n' + 1 => do
    let res ← make_conjunction_of_holes headingop n'
    `(tlafml| ($headingop:tlafml_heading_op ($q:term)) ∧ $res:tlafml )

def make_conjunction_of_terms (tms : List (TSyntax `term)) : MacroM (TSyntax `term) := do
  match tms with
  | [] => Macro.throwUnsupported
  | [t] => `(term| $t)
  | t :: tms' =>
    let res ← make_conjunction_of_terms tms'
    `(term| And.intro $t ($res) )

partial def splitAndIntoParts (p : Expr) : MetaM (List Expr) := do
  match_expr p with
  | TLA.tla_and _ a b =>
    let as ← splitAndIntoParts a
    let bs ← splitAndIntoParts b
    pure (as ++ bs)
  | _ => pure [p]

partial def splitImplicationsIntoParts (p : Expr) : MetaM (List Expr × Expr) := do
  match_expr p with
  | TLA.tla_implies _ p q =>
    let ps ← splitAndIntoParts p
    let (ps', q') ← splitImplicationsIntoParts q
    pure (ps ++ ps', q')
  | _ => pure ([], p)

def splitPredImpliesIntoParts (p : Expr) : MetaM (List Expr × Expr) := do
  match_expr p with
  | TLA.pred_implies _ p q =>
    let ps ← splitAndIntoParts p
    let (ps', q') ← splitImplicationsIntoParts q
    pure (ps ++ ps', q')
  | TLA.valid _ body => splitImplicationsIntoParts body
  | _ => throwError "not a |-tla- statement"

def peekStateType (p : Expr) : Option Expr :=
  match_expr p with
  | TLA.pred_implies σ _ _ => .some σ
  | TLA.valid σ _ => .some σ
  | _ => .none

def assembleUnderCommonContextShape (σ : Expr) (ps : List Expr) (q : Expr) : MetaM Expr := do
  withLocalDeclD `Γ (← mkAppM ``TLA.pred #[σ]) fun Γ => do
    let ps' ← ps.toArray.mapM fun p => mkAppM ``TLA.pred_implies #[Γ, p]
    let q' ← mkAppM ``TLA.pred_implies #[Γ, q]
    let body ← mkArrowN ps' q'
    mkForallFVars #[Γ] body

partial def assembleSeparatedPredImplications (ps : List Expr) (q : Expr) : MetaM Expr := do
  let build p := do
    let (ps, q) ← simplify [] p
    match List.getLast? ps with
    | none => mkAppM ``TLA.valid #[q]
    | some p =>
      let ps := List.dropLast ps
      let conj ← ps.foldrM (fun pp conj => mkAppM ``TLA.tla_and #[pp, conj]) p
      mkAppM ``TLA.pred_implies #[conj, q]
  let ps' ← ps.mapM build
  let q' ← build q
  let res ← mkArrowN ps'.toArray q'
  pure res
where simplify (ps : List Expr) (q : Expr) : MetaM (List Expr × Expr) := do
  
  
  
  
  match_expr q with
  | TLA.always_implies _ a b =>
    if ps.isEmpty then
      simplify [] (← mkAppM ``TLA.tla_implies #[a, b])
    else
      pure (ps, q)
  | TLA.tla_implies _ _ _ =>
    let (ps', q') ← splitImplicationsIntoParts q
    pure (ps ++ ps', q')
  | _ => pure (ps, q)

def deriveForPredImpliesOrValid (nm : Name) : CoreM Unit := do
  
  let info ← getConstInfo nm
  let ty := info.type
  let lvlParams := info.levelParams
  let noncomputable? := isNoncomputable (← getEnv) nm
  MetaM.run' do
    let (thmName1, thmStmt1, thmName2, thmStmt2) ←
      forallTelescope ty fun xs body => do
        let (ps, q) ← splitPredImpliesIntoParts body
        let .some σ := peekStateType body | unreachable!
        
        let thmStmt1 ← assembleUnderCommonContextShape σ ps q
        let thmStmt1 ← mkForallFVars xs thmStmt1
        let thmName1 := nm ++ `with_context

        let thmStmt2 ← assembleSeparatedPredImplications ps q
        let thmStmt2 ← mkForallFVars xs thmStmt2
        let thmName2 := nm ++ `weakened
        pure (thmName1, thmStmt1, thmName2, thmStmt2)

    simpleProveTheorem thmName1 lvlParams thmStmt1
      
      
      
      
      (← `(term| by admit /- proof elided -/
        )) noncomputable?
    simpleProveTheorem thmName2 lvlParams thmStmt2
      (← do
        let htmp ← mkIdent <$> mkFreshUserName `htmp
        let htmp' ← mkIdent <$> mkFreshUserName `htmp'
        let introNames ← ty.getForallBinderNames.toArray.mapM (mkIdent <$> mkFreshUserName ·)
        `(term| by admit /- proof elided -/
          )) noncomputable?

def exec (σ : Type u) := Nat → σ

def pred (σ : Type u) := exec σ → Prop

def state_pred {σ : Type u} (f : σ → Prop) : pred σ :=
  fun e => f (e 0)

def action (σ : Type u) := σ → σ → Prop

def action_pred {σ : Type u} (a : action σ) : pred σ :=
  fun e => a (e 0) (e 1)

def pure_pred {α : Type u} (p : Prop) : pred α := state_pred (fun _ => p)

def tla_true {α : Type u} : pred α := pure_pred True

def tla_false {α : Type u} : pred α := pure_pred False

def tla_and {α : Type u} (p q : pred α) : pred α := fun σ => p σ ∧ q σ

def tla_or {α : Type u} (p q : pred α) : pred α := fun σ => p σ ∨ q σ

def tla_implies {α : Type u} (p q : pred α) : pred α := fun σ => p σ → q σ

def tla_not {α : Type u} (p : pred α) : pred α := fun σ => ¬ p σ

def tla_forall {α : Sort u} {β : Type v} (p : α → pred β) : pred β := fun σ => ∀ x, p x σ

def tla_exists {α : Sort u} {β : Type v} (p : α → pred β) : pred β := fun σ => ∃ x, p x σ

instance {α : Type u} : Std.Commutative (@tla_and α) :=

instance {α : Type u} : Std.Associative (@tla_and α) :=

instance {α : Type u} : Std.Commutative (@tla_or α) :=

instance {α : Type u} : Std.Associative (@tla_or α) :=

def exec.drop {α : Type u} (k : Nat) (σ : exec α) : exec α := λ n => σ (n + k)

def exec.take {α : Type u} (k : Nat) (σ : exec α) : List α := List.range k |>.map σ

def exec.take_from {α : Type u} (start k : Nat) (σ : exec α) : List α := List.range' start k |>.map σ

def always {α : Type u} (p : pred α) : pred α := λ σ => ∀ k, p <| σ.drop k

def eventually {α : Type u} (p : pred α) : pred α := λ σ => ∃ k, p <| σ.drop k

def later {α : Type u} (p : pred α) : pred α := λ σ => p <| σ.drop 1

def exec.satisfies {α : Type u} (p : pred α) (σ : exec α) : Prop := p σ

def valid {α : Type u} (p : pred α) : Prop := ∀ (σ : exec α), σ.satisfies p

def pred_implies {α : Type u} (p q : pred α) : Prop := ∀ (σ : exec α), σ.satisfies p → σ.satisfies q

def enabled {α : Type u} (a : action α) (s : α) : Prop := ∃ s', a s s'

def tla_enabled {α : Type u} (a : action α) : pred α := state_pred (enabled a)

class Foldable (c : Type u → Type v) where
  fold {α : Type u} {β : Type w} (op : β → β → β) [Std.Commutative op] [Std.Associative op]
    (b : β) (f : α → β) (s : c α) : β

instance : Foldable List where
  fold op _ _ b f s := List.foldr (op <| f ·) b s

def tla_bigwedge {α : Type u} {β : Type v} {c} [Foldable c] (f : β → pred α) (s : c β) : pred α :=
  Foldable.fold tla_and tla_true f s

def tla_bigvee {α : Type u} {β : Type v} {c} [Foldable c] (f : β → pred α) (s : c β) : pred α :=
  Foldable.fold tla_or tla_false f s

def tla_until {α : Type u} (p q : pred α) : pred α := λ σ => ∃ i, (q <| σ.drop i) ∧ ∀ j < i, (p <| σ.drop j)

def TLA.leads_to {α : Type u} (p q : TLA.pred α) : TLA.pred α := [tlafml| □ (p → ◇ q) ]

def TLA.always_implies {α : Type u} (p q : TLA.pred α) : TLA.pred α := [tlafml| □ (p → q) ]

def TLA.weak_fairness {α : Type u} (a : action α) : pred α := [tlafml| □ ((□ (Enabled a)) → ◇ ⟨a⟩)]

def TLA.syntax_term_to_tlafml [Monad m] [MonadQuotation m] (stx : TSyntax `term) : m (TSyntax `tlafml) := do
  match stx with
  | `([tlafml| $f:tlafml ]) => pure f
  | `(term|$t:term) => `(tlafml| $t:term )

def TLA.syntax_tlafml_to_term [Monad m] [MonadQuotation m] (stx : TSyntax `tlafml) : m (TSyntax `term) := do
  match stx with
  | `(tlafml| $t:term ) => pure t
  | f => `(term|[tlafml| $f:tlafml ])

def annAsTerm {any} (stx : TSyntax any) : DelabM (TSyntax any) :=
  (⟨·⟩) <$> annotateTermInfo ⟨stx.raw⟩

partial def delab_tlafml_inner : DelabM (TSyntax `tlafml) := do
  let e ← getExpr
  let stx ← do
     
    
    
    
    let fn := e.getAppFn'.constName
    match fn with
    | ``TLA.tla_true => `(tlafml| ⊤ )
    | ``TLA.tla_false => `(tlafml| ⊥ )
    | ``TLA.state_pred | ``TLA.pure_pred | ``TLA.action_pred | ``TLA.tla_enabled | ``TLA.weak_fairness =>
      let t ← withAppArg delab
      match fn with
      | ``TLA.state_pred => `(tlafml| ⌜ $t:term ⌝ )
      | ``TLA.pure_pred => `(tlafml| ⌞ $t:term ⌟ )
      | ``TLA.action_pred => `(tlafml| ⟨ $t:term ⟩ )
      | ``TLA.tla_enabled => `(tlafml| Enabled $t:term )
      | ``TLA.weak_fairness => `(tlafml| 𝒲ℱ $t:term )
      | _ => unreachable!
    | ``TLA.tla_not | ``TLA.always | ``TLA.eventually | ``TLA.later =>
      let f ← withAppArg delab_tlafml_inner
      match fn with
      | ``TLA.tla_not => `(tlafml| ¬ $f:tlafml )
      | ``TLA.always => `(tlafml| □ $f:tlafml )
      | ``TLA.eventually => `(tlafml| ◇ $f:tlafml )
      | ``TLA.later => `(tlafml| ◯ $f:tlafml )
      | _ => unreachable!
    | ``TLA.tla_and | ``TLA.tla_or | ``TLA.tla_implies | ``TLA.leads_to | ``TLA.tla_until | ``TLA.always_implies =>
      let f1 ← withAppFn <| withAppArg delab_tlafml_inner
      let f2 ← withAppArg delab_tlafml_inner
      match fn with
      | ``TLA.tla_and => `(tlafml| $f1:tlafml ∧ $f2:tlafml)
      | ``TLA.tla_or => `(tlafml| $f1:tlafml ∨ $f2:tlafml)
      | ``TLA.tla_implies => `(tlafml| $f1:tlafml → $f2:tlafml)
      | ``TLA.leads_to => `(tlafml| $f1:tlafml ↝ $f2:tlafml)
      | ``TLA.tla_until => `(tlafml| $f1:tlafml 𝑈 $f2:tlafml)
      | ``TLA.always_implies => `(tlafml| $f1:tlafml ⇒ $f2:tlafml)
      | _ => unreachable!
    | ``TLA.tla_forall | ``TLA.tla_exists =>
       
      let body ← withAppArg delab
      let (a, stx) ← get_bindername_funbody body
      match fn with
      | ``TLA.tla_forall => do `(tlafml| ∀ $a:ident, $stx )
      | ``TLA.tla_exists => do `(tlafml| ∃ $a:ident, $stx )
      | _ => unreachable!
    | ``TLA.tla_bigwedge | ``TLA.tla_bigvee =>
      let body ← withAppFn <| withAppArg delab
      let l ← withAppArg delab
      let (a, stx) ← get_bindername_funbody body
      match fn with
      | ``TLA.tla_bigwedge => do `(tlafml| ⋀ $a:ident ∈ $l, $stx )
      | ``TLA.tla_bigvee => do `(tlafml| ⋁ $a:ident ∈ $l, $stx )
      | _ => unreachable!
    | _ =>
      
      `(tlafml| $(← delab):term )
  annAsTerm stx
where get_bindername_funbody (body : Term) : DelabM (Ident × TSyntax `tlafml) := do
  match body with
  | `(fun $a:ident => $stx) | `(fun ($a:ident : $_) => $stx) => pure (a, (← TLA.syntax_term_to_tlafml stx))
  | _ =>
    
    
    let x := mkIdent <| .mkSimple "x"
    let bodyapp ← `(term| $body $x )
    pure (x, (← `(tlafml| $bodyapp:term )))

partial def delab_tlafml : Delab := whenPPOption (fun o => o.get lentil.pp.useDelab.name true) do
  let e ← getExpr
  let fn := e.getAppFn.constName
  
  let check_applicable (offset : Nat) :=
    (List.elem fn [``TLA.state_pred, ``TLA.pure_pred, ``TLA.action_pred, ``TLA.tla_enabled, ``TLA.weak_fairness,
        ``TLA.tla_not, ``TLA.always, ``TLA.eventually, ``TLA.later]
      && e.getAppNumArgs' == 2 + offset) ||
    (List.elem fn [``TLA.tla_and, ``TLA.tla_or, ``TLA.tla_implies, ``TLA.leads_to, ``TLA.tla_until, ``TLA.always_implies,
        ``TLA.tla_forall, ``TLA.tla_exists]
      && e.getAppNumArgs' == 3 + offset) ||
    (List.elem fn [``TLA.tla_true, ``TLA.tla_false]
      && e.getAppNumArgs' == 1 + offset) ||
    (List.elem fn [``TLA.tla_bigwedge, ``TLA.tla_bigvee]
      && e.getAppNumArgs' == 6 + offset)
  if check_applicable 0
  then delab_tlafml_inner >>= TLA.syntax_tlafml_to_term
  else whenPPOption (fun o => o.get lentil.pp.autoRenderSatisfies.name true) do
    if check_applicable 1
    then
      let res ← withAppFn delab_tlafml_inner
      let e ← withAppArg delab
      `(term| $e |=tla= $res)
    else failure

@[app_unexpander TLA.pred_implies] def TLA.unexpand_pred_implies : Lean.PrettyPrinter.Unexpander
  | `($_ $stx1 $stx2) => do `(($(← TLA.syntax_term_to_tlafml stx1)) |-tla- ($(← TLA.syntax_term_to_tlafml stx2)))
  | _ => throw ()

@[app_unexpander TLA.valid] def TLA.unexpand_valid : Lean.PrettyPrinter.Unexpander
  | `($_ $stx) => do `(|-tla- ($(← TLA.syntax_term_to_tlafml stx)))
  | _ => throw ()

@[app_unexpander TLA.exec.satisfies] def TLA.unexpand_satisfies : Lean.PrettyPrinter.Unexpander
  | `($_ $stx1 $stx2) => do `($stx2 |=tla= $(← TLA.syntax_term_to_tlafml stx1))
  | _ => throw ()

@[app_unexpander Eq] def TLA.unexpand_tla_eq : Lean.PrettyPrinter.Unexpander
  | `($_ [tlafml| $f1:tlafml ] [tlafml| $f2:tlafml ]) => `(($f1) =tla= ($f2))
  | `($_ [tlafml| $f1:tlafml ] $t2:term) => do `(($f1) =tla= ($(← `(tlafml| $t2:term ))))
  | `($_ $t1:term [tlafml| $f2:tlafml ]) => do `(($(← `(tlafml| $t1:term ))) =tla= ($f2))
  | _ => throw ()       

@[category_parenthesizer tlafml]
def tlafml.parenthesizer : CategoryParenthesizer | prec => do
  maybeParenthesize `tlafml true wrapParens prec $
    parenthesizeCategoryCore `tlafml prec
where
  wrapParens (stx : Syntax) : Syntax := Unhygienic.run do
    let pstx ← `(($(⟨stx⟩)))
    return pstx.raw.setInfo (SourceInfo.fromRef stx)

Nat in Init.Prelude

Std.Commutative in Init.Core

Std.Associative in Init.Core

List in Init.Prelude

List.range in Init.Data.List.Basic

List.range' in Init.Data.List.Basic

id in Init.Prelude

List.foldr in Init.Data.List.Basic

List.finRange in Init.Data.List.FinRange

Lean.MonadQuotation in Init.Prelude

Lean.TSyntax in Init.Prelude

Monad in Init.Prelude

Lean.mkIdent in Init.Meta.Defs

List.elem in Init.Data.List.Basic

Lean.PrettyPrinter.Unexpander in Init.Prelude

Eq in Init.Prelude

Lean.SourceInfo.fromRef in Init.Prelude

Lean.Syntax in Init.Prelude

Lean.Unhygienic.run in Lean.Hygiene

Lean.MacroM in Init.Prelude

Lean.Macro.throwUnsupported in Init.Prelude

And in Init.Prelude

Lean.Expr in Lean.Expr

Lean.mkApp in Lean.Expr

Lean.MVarId in Lean.Expr

Array in Init.Prelude

Array.range in Init.Data.Array.Basic

Lean.Name.mkSimple in Init.Prelude

Lean.getLocalHyps in Lean.LocalContext

List.replicate in Init.Data.List.Basic

Unit in Init.Prelude

Lean.instantiateMVars in Lean.MetavarContext

Lean.FVarId in Lean.Expr

Lean.mkConst in Lean.Expr

Lean.throwError in Lean.Exception

Lean.Parser.Term.funBinder in Lean.Parser.Term

Lean.binderIdent in Init.Notation

Fin in Init.Prelude

Nat.strongRecOn in Init.WF

Bool in Init.Prelude

Lean.Name in Init.Prelude

Lean.Declaration.thmDecl in Lean.Declaration

Lean.addAndCompile in Lean.AddDecl

Lean.addDecl in Lean.AddDecl

Lean.addNoncomputable in Lean.Compiler.NoncomputableAttr

Lean.mkTheoremValEx in Lean.Declaration

Lean.setEnv in Lean.MonadEnv

Lean.liftCommandElabM in Lean.Elab.Command

Lean.trace in Lean.Util.Trace

Lean.Name.appendIndexAfter in Init.Meta.Defs

List.length in Init.Prelude

Lean.Meta.isProp in Lean.Meta.InferType

Lean.AssocList in Lean.Data.AssocList

Exists in Init.Core

Not in Init.Prelude

Or in Init.Prelude

Iff in Init.Core

Inhabited in Init.Prelude

ToString in Init.Data.ToString.Basic

Decidable in Init.Prelude

DecidableEq in Init.Prelude

DecidablePred in Init.Prelude

Lean.BinderInfo.implicit in Lean.Expr

Lean.mkLevelParam in Lean.Level

Lean.mkLevelSucc in Lean.Level

Array.append in Init.Data.Array.Basic

Prod in Init.Prelude

Prod.snd in Init.Prelude

Lean.getConstInfo in Lean.MonadEnv

Option in Init.Prelude

Lean.isNoncomputable in Lean.Compiler.NoncomputableAttr

propext in Init.Core

Lean.mkArrowN in Lean.CoreM

List.getLast? in Init.Data.List.Basic

List.dropLast in Init.Data.List.Basic
</all_available_defs>

<all_available_lemmas>
theorem state_preds_and (p q : σ → Prop) : (⌜ p ⌝ ∧ ⌜ q ⌝) =tla= ⌜ λ s => p s ∧ q s ⌝

theorem init_invariant {init : σ → Prop} {next : action σ} {inv : σ → Prop}
    (hinit : ∀ s, init s → inv s)
    (hnext : ∀ s s', next s s' → inv s → inv s') :
  (⌜ init ⌝ ∧ □ ⟨next⟩) |-tla- (□ ⌜ inv ⌝)

theorem wf1' (p q init inv : σ → Prop) (next a : action σ)
  (hpuntilq : ∀ s s', p s → next s s' → p s' ∨ q s')
  (haq : ∀ s s', p s → next s s' → a s s' → q s')
  (henable : ∀ s, inv s → p s → enabled a s ∨ q s)
  (hinit_inv : ∀ s, init s → inv s)
  (hnext_inv : ∀ s s', next s s' → inv s → inv s') :
  (⌜ init ⌝ ∧ □ ⟨next⟩ ∧ 𝒲ℱ a) |-tla- (⌜ p ⌝ ↝ ⌜ q ⌝)

theorem wf_as_leads_to : (𝒲ℱ a) =tla= (□ Enabled a ↝ ⟨a⟩)

theorem mem_forall_iff_fin_index {α : Type u} (l : List α) (p : α → Prop) :
  (∀ x, x ∈ l → p x) ↔ ∀ (x : Fin l.length), p l[x]

theorem mem_exists_iff_fin_index {α : Type u} (l : List α) (p : α → Prop) :
  (∃ x, x ∈ l ∧ p x) ↔ ∃ (x : Fin l.length), p l[x]

theorem finRange_fin_in (n : Nat) : ∀ (x : Fin n), x ∈ List.finRange n

theorem find_min {p : Nat → Prop} (n : Nat) (h : p n) :
  ∃ n', n' ≤ n ∧ p n' ∧ ∀ m, m < n' → ¬ p m

theorem find_min' {p : Nat → Prop} (n : Nat) (h : p n) :
  ∃ n', n' ≤ n ∧ p n' ∧ ∀ m, p m → n' ≤ m

@[tlasimp]
theorem bigwedge_list_nil : (⋀ x ∈ [], (f x)) =tla= (⊤)

@[tlasimp]
theorem bigwedge_list_cons (b : β) : (⋀ x ∈ (b :: l), (f x)) =tla= ((f b) ∧ ⋀ x ∈ l, (f x))

theorem bigwedge_forall_list : (⋀ x ∈ l, (f x)) =tla= (∀ x, (⌞ x ∈ l ⌟ → (f x)))

theorem bigwedge_forall_fintype_list : (⋀ x ∈ l, (f x)) =tla= (∀ x : Fin l.length, (f l[x]))

theorem bigwedge_inner_and_split : (⋀ x ∈ l, (f x) ∧ (g x)) =tla= ((⋀ x ∈ l, (f x)) ∧ (⋀ x ∈ l, (g x)))

theorem always_bigwedge : (□ ⋀ x ∈ l, (f x)) =tla= (⋀ x ∈ l, □ (f x))

theorem eventually_always_bigwedge_distrib : (◇ □ ⋀ x ∈ l, (f x)) =tla= (⋀ x ∈ l, ◇ □ (f x))

@[tlasimp]
theorem bigvee_list_nil : (⋁ x ∈ [], (f x)) =tla= (⊥)

@[tlasimp]
theorem bigvee_list_cons (b : β) : (⋁ x ∈ (b :: l), (f x)) =tla= ((f b) ∨ ⋁ x ∈ l, (f x))

theorem bigvee_exists_list : (⋁ x ∈ l, (f x)) =tla= (∃ x, (⌞ x ∈ l ⌟ ∧ (f x)))

theorem bigvee_exists_fintype_list : (⋁ x ∈ l, (f x)) =tla= (∃ x : Fin l.length, (f l[x]))

theorem bigvee_and_distrib (p : pred α) : (p ∧ ⋁ x ∈ l, (f x)) =tla= (⋁ x ∈ l, p ∧ (f x))

theorem bigwedge_bigvee_match : ((⋀ x ∈ l, (f x)) ∧ (⋁ x ∈ l, (g x))) |-tla- (⋁ x ∈ l, (f x) ∧ (g x))

theorem dual_lemma (p q : pred σ) : ¬ p =tla= ¬ q → (p) =tla= (q)

theorem pred_eq_iff_iff (p q : pred σ) : (p) =tla= (q) ↔ (p) |-tla- (q) ∧ (q) |-tla- (p)

theorem impl_intro (p q : pred σ) : |-tla- (p → q) = (p) |-tla- (q)

theorem impl_decouple (p q : pred σ) : |-tla- (p → q) → |-tla- (p) → |-tla- (q)

theorem and_pred_implies_split (Γ p q : pred σ) : (Γ) |-tla- (p ∧ q) = ((Γ) |-tla- (p) ∧ (Γ) |-tla- (q))

theorem and_valid_split (p q : pred σ) : |-tla- (p ∧ q) = (|-tla- (p) ∧ |-tla- (q))

theorem impl_intro_add_r (p q r : pred σ) : (r) |-tla- (p → q) = (r ∧ p) |-tla- (q)

theorem impl_drop_hyp (p q : pred σ) : |-tla- (q) → (p) |-tla- (q)

theorem impl_drop_hyp_one_r (p q r : pred σ) : (p) |-tla- (q) → (p ∧ r) |-tla- (q)

theorem always_intro : (|-tla- (p)) = (|-tla- (□ p))

theorem later_always_comm : (◯ □ p) =tla= (□ ◯ p)

theorem always_unroll : □ p =tla= (p ∧ ◯ □ p)

theorem always_induction : □ p =tla= (p ∧ □ (p → ◯ p))

theorem always_weaken : □ p |-tla- (p)

theorem always_weaken_to_eventually : □ p |-tla- ◇ p

theorem later_weaken_to_eventually : ◯ p |-tla- ◇ p

theorem now_weaken_to_eventually : (p) |-tla- ◇ p

theorem not_always : (¬ □ p) =tla= (◇ ¬ p)

@[tladual]
theorem not_eventually : (¬ ◇ p) =tla= □ ¬ p

theorem eventually_to_always : ◇ p =tla= ¬ □ ¬ p

@[tladual]
theorem always_to_eventually : □ p =tla= ¬ ◇ ¬ p

theorem always_idem : (□ □ p) =tla= □ p

@[tladual]
theorem eventually_idem : (◇ ◇ p) =tla= ◇ p

theorem always_eventually_always : (□ ◇ □ p) =tla= ◇ □ p

@[tladual]
theorem eventually_always_eventually : (◇ □ ◇ p) =tla= □ ◇ p

theorem always_eventually_idem : (□ ◇ □ ◇ p) =tla= □ ◇ p

@[tladual]
theorem eventually_always_idem : (◇ □ ◇ □ p) =tla= ◇ □ p

theorem contraposition_for_pred_implies : (p) |-tla- (q) = ((¬ q) |-tla- ¬ p)

theorem proof_by_contra : (p) |-tla- (q) = (¬ q ∧ p) |-tla- (⊥)

theorem modus_ponens : (p ∧ (p → q)) |-tla- (q)

theorem modus_ponens_with_premise : (p ∧ (p → q)) |-tla- (p ∧ q)

theorem always_and_eventually : (◇ p ∧ □ q) |-tla- (◇ (p ∧ q))

theorem always_and_eventually' : (◇ p ∧ □ q) |-tla- (◇ (p ∧ □ q))

theorem later_monotone : (p) |-tla- (q) → ◯ p |-tla- ◯ q

theorem always_monotone : (p) |-tla- (q) → □ p |-tla- □ q

theorem eventually_monotone : (p) |-tla- (q) → ◇ p |-tla- ◇ q

theorem always_eventually_monotone : (p) |-tla- (q) → (□ ◇ p) |-tla- (□ ◇ q)

theorem eventually_always_monotone : (p) |-tla- (q) → (◇ □ p) |-tla- (◇ □ q)

theorem until_induction : (p ∧ □ (p ∧ ¬ q → ◯ p)) |-tla- ((□ (p ∧ ¬ q)) ∨ (p 𝑈 (p ∧ q)))

theorem later_forall : (◯ ∀ x, (p x)) =tla= (∀ x, ◯ (p x))

theorem later_exists : (◯ ∃ x, (p x)) =tla= (∃ x, ◯ (p x))

theorem always_forall : (□ ∀ x, (p x)) =tla= (∀ x, □ (p x))

theorem eventually_exists : (◇ ∃ x, (p x)) =tla= (∃ x, ◇ (p x))

theorem exists_into_always : (∃ x, □ (p x)) |-tla- □ (∃ x, (p x))

@[tladual]
theorem eventually_into_forall : (◇ ∀ x, (p x)) |-tla- (∀ x, ◇ (p x))

theorem later_and : (◯ (p ∧ q)) =tla= (◯ p ∧ ◯ q)

theorem later_or : (◯ (p ∨ q)) =tla= (◯ p ∨ ◯ q)

theorem always_and : (□ (p ∧ q)) =tla= (□ p ∧ □ q)

@[tladual]
theorem eventually_or : (◇ (p ∨ q)) =tla= (◇ p ∨ ◇ q)

theorem always_or_merge : (□ p ∨ □ q) |-tla- □ (p ∨ q)

@[tladual]
theorem eventually_and_split : (◇ (p ∧ q)) |-tla- (◇ p ∧ ◇ q)

theorem eventually_always_and_distrib : (◇ □ (p ∧ q)) =tla= (◇ □ p ∧ ◇ □ q)

@[tladual]
theorem always_eventually_or_distrib : (□ ◇ (p ∨ q)) =tla= (□ ◇ p ∨ □ ◇ q)

theorem leads_to_exists (Γ q : pred σ) (p : α → pred σ) :
  (∀ (x : α), (Γ) |-tla- ((p x) ↝ q)) ↔ (Γ) |-tla- ((tla_exists p) ↝ q)

theorem leads_to_pure_pred_and (Γ p q : pred σ) (φ : Prop) :
  (φ → (Γ) |-tla- (p ↝ q)) ↔ (Γ) |-tla- (⌞ φ ⌟ ∧ p ↝ q)

@[tla_derive]
theorem leads_to_conseq (p p' q q': pred σ) :
  |-tla- ((p' ⇒ p) → (q ⇒ q') → (p ↝ q) ⇒ (p' ↝ q'))

@[tla_derive]
theorem leads_to_trans (p q r : pred σ) :
  |-tla- ((p ↝ q) → (q ↝ r) → (p ↝ r))

theorem leads_to_combine (Γ Γ' p1 q1 p2 q2 : pred σ)
  (h1 : (□ Γ ∧ Γ') |-tla- (p1 ↝ q1))
  (h2 : (□ Γ ∧ Γ') |-tla- (p2 ↝ q2))
  (h1' : (q1 ∧ □ Γ) |-tla- □ q1) (h2' : (q2 ∧ □ Γ) |-tla- □ q2) :
  (□ Γ ∧ Γ') |-tla- (p1 ∧ p2 ↝ q1 ∧ q2)

@[tla_derive]
theorem leads_to_strengthen_lhs (p q inv : pred σ) :
  |-tla- (□ inv → (p ∧ inv ↝ q) → (p ↝ q))

theorem exec.drop_drop {α : Type u} (k l : Nat) (σ : exec α) : (σ.drop k).drop l = σ.drop (k + l)

@[refl] theorem pred_implies_refl {α : Type u} (p : pred α) : pred_implies p p

theorem pred_implies_trans {p q r : pred α} : pred_implies p q → pred_implies q r → pred_implies p r

theorem Foldable.list_index_form_change {α : Type u} {β : Type w} (op : β → β → β) [inst1 : Std.Commutative op] [inst2 : Std.Associative op]
    (b : β) (f : α → β) (l : List α) :
  Foldable.fold op b f l = Foldable.fold op b (f <| l[·]) (List.finRange l.length)
</all_available_lemmas>

<local_ctx>
import Lentil.Rules.Basic

import Lentil.Tactics.Structural

import Lentil.Gadgets.TheoremDeriving

open Classical

namespace TLA

section wf

variable {σ : Type u}

section wf_def

variable {a : action σ}

end wf_def
</local_ctx>

<target_theorem>
@[tla_derive]
theorem wf1 (p q : pred σ) (next a : action σ) :
  ((p ∧ ⟨next⟩ ⇒ ◯ p ∨ ◯ q) ∧
   (p ∧ ⟨next⟩ ∧ ⟨a⟩ ⇒ ◯ q) ∧
   (p ⇒ Enabled a ∨ q) ∧
   (□ ⟨next⟩ ∧ 𝒲ℱ a)) |-tla- (p ↝ q) :=
</target_theorem>

