inductive Cvc.AfterZero (α : Nat → Type) (n : Nat) : Type

• zero {α : Nat → Type} : AfterZero α 0
• mk {α : Nat → Type} {k : Nat} (get : α k) : AfterZero α k.succ

@[reducible, inline]

abbrev Cvc.AfterZero' (α : Type) (n : Nat) : Type

Equations

• Cvc.AfterZero' α n = Cvc.AfterZero (Cvc.𝕂 α) n

def Cvc.AfterZero.get {α : Nat → Type} {k : Nat} : AfterZero α k.succ → α k

Equations

• (Cvc.AfterZero.mk get).get = get

instance Cvc.AfterZero.instCoeDep {α : Nat → Type} {k : Nat} {az : AfterZero α k.succ} : CoeDep (AfterZero α k.succ) az (α k)

Equations

• Cvc.AfterZero.instCoeDep = { coe := az.get }

def Cvc.AfterZero.nextM {m : Type → Type u_1} {α : Nat → Type} {n : Nat} [Monad m] (next : α n → m (α n.succ)) : AfterZero α n.succ → m (AfterZero α n.succ.succ)

Equations

• Cvc.AfterZero.nextM next (Cvc.AfterZero.mk get) = do let __do_lift ← next get pure (Cvc.AfterZero.mk __do_lift)

def Cvc.AfterZero.next {α : Nat → Type} {n : Nat} (next : α n → α n.succ) (az : AfterZero α n.succ) : AfterZero α n.succ.succ

Equations

• Cvc.AfterZero.next next az = Cvc.AfterZero.nextM next az

def Cvc.AfterZero.nextM' {m : Type → Type u_1} {α : Type} {n : Nat} [Monad m] (atZero : m α) : AfterZero' α n → m (AfterZero' α n.succ)

Equations

• Cvc.AfterZero.nextM' atZero Cvc.AfterZero.zero = Cvc.AfterZero.mk <$> atZero
• Cvc.AfterZero.nextM' atZero (Cvc.AfterZero.mk val) = pure (Cvc.AfterZero.mk val)

def Cvc.AfterZero.next' {α : Type} {n : Nat} (az : AfterZero' α n.succ) (next : α → α := id) : AfterZero' α n.succ.succ

Equations

• Cvc.AfterZero.next' az next = Cvc.AfterZero.next next az

structure Cvc.Sys {Struct : Symbols.Repr} (State : Symbols Struct) (depth : Nat := 0) : Type

• mk' :: (
• toUnroller : State.Unroller depth
• candidates : Candidates State depth
• )

def Cvc.Sys.mk {S : Symbols.Repr} [State : Symbols S] (idents : Symbols.Idents) (init : Symbols.StatePred) (step : Symbols.StateRel) (candidates : Symbols.NamedPredicates := RBMap.empty) : Sys State

Equations

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

def Cvc.Sys.depth {S : Symbols.Repr} [State : Symbols S] {depth : Nat} (sys : Sys State depth) : Nat

Equations

• Cvc.Sys.depth = Cvc.𝕂 depth

def Cvc.Sys.toLines {S : Symbols.Repr} [State : Symbols S] {depth : Nat} (sys : Sys State depth) (pref : String := "") : Array String

Equations

• sys.toLines pref = Cvc.Sys.Candidates.toLines pref sys.candidates

def Cvc.Sys.addCandidate {S : Symbols.Repr} [State : Symbols S] (sys : Sys State) (name : String) (pred : Symbols.StatePred) : Res (Sys State)

Equations

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

def Cvc.Sys.addCandidates {S : Symbols.Repr} [State : Symbols S] {α : Type u_1} [ForIn Res α (String × Symbols.StatePred)] (sys : Sys State) (candidates : α) : Res (Sys State)

Equations

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

def Cvc.Sys.getUnknownCandidates {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Candidate.UnknownMap State depth

Equations

• sys.getUnknownCandidates = sys.candidates.unknown

@[reducible, inline]

abbrev Cvc.Sys.isDone {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Bool

Equations

• sys.isDone = sys.candidates.isDone

@[reducible, inline]

abbrev Cvc.Sys.isNextBaseReady {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Bool

Equations

• sys.isNextBaseReady = sys.candidates.isNextBaseReady

@[reducible, inline]

abbrev Cvc.Sys.isNextStepReady {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Bool

Equations

• sys.isNextStepReady = sys.candidates.isNextStepReady

@[reducible, inline]

abbrev Cvc.Sys.isNextReady {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Bool

Equations

• sys.isNextReady = decide (sys.isNextBaseReady = true ∧ sys.isNextStepReady = true)

@[reducible, inline]

abbrev Cvc.Sys.isBaseOver {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Bool

Equations

• sys.isBaseOver = sys.isNextBaseReady

@[reducible, inline]

abbrev Cvc.Sys.isStepOver {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Bool

Equations

• sys.isStepOver = sys.isNextStepReady

def Cvc.Sys.getStateAt {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) (k : Nat) (h : k < depth := by omega) : Symbols.TermsAt k

Equations

• sys.getStateAt k h = Cvc.Symbols.Trace.get sys.toUnroller.trace k h

def Cvc.Sys.getState0 {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth.succ) : Symbols.TermsAt 0

Equations

• sys.getState0 = sys.getStateAt 0 ⋯

def Cvc.Sys.getLatestState {S : Symbols.Repr} [State : Symbols S] {k : Nat} (sys : Sys State (k + 1)) : Symbols.TermsAt k

Equations

• sys.getLatestState = sys.getStateAt k ⋯

def Cvc.Sys.unroll' {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) : Smt (Sys State depth.succ)

Equations

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

def Cvc.Sys.unroll {S : Symbols.Repr} {depth : Nat} [State : Symbols S] (sys : Sys State depth) (h : ¬sys.isDone = true := by (try simp [*] <;> assumption)) : Smt (Sys State depth.succ)

Equations

• sys.unroll x✝ = sys.unroll'

@[irreducible]

def Cvc.Sys.checkBase {S : Symbols.Repr} [State : Symbols S] {k : Nat} (sys : Sys State k.succ) (h : ¬sys.isBaseOver = true := by (try simp; done) <;> assumption) (maxIter : Nat := (Batteries.RBMap.size sys.candidates.unknown).succ) : Smt (Sys State k.succ)

Equations

• One or more equations did not get rendered due to their size.
• sys.checkBase x 0 = Cvc.throwInternal (toString "base-checking at `" ++ toString k ++ toString "` not done after number-of-candidates-plus-one iterations")

@[irreducible]

def Cvc.Sys.checkStep {S : Symbols.Repr} [State : Symbols S] {k : Nat} (sys : Sys State k.succ.succ) (h : ¬sys.isStepOver = true := by (try simp; done) <;> assumption) (maxIter maxIterRef : Nat := Batteries.RBMap.size sys.candidates.unknown) : Smt (Sys State k.succ.succ)

Equations

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

def Cvc.Sys.unrollCheckBaseStep {S : Symbols.Repr} [State : Symbols S] {k : Nat} (sys : Sys State k) (h_base : sys.isBaseOver = true := by (try simp; done) <;> assumption) (h_step : sys.isStepOver = true := by (try simp; done) <;> assumption) (h : ¬sys.isDone = true := by (try simp; done) <;> assumption) : Smt (Sys State k.succ)

Equations

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

def Cvc.Sys.kInduction {S : Symbols.Repr} [State : Symbols S] {k : Nat} (sys : Sys State k) (maxSteps : Nat) : Smt ((k' : Nat) × Sys State k'.succ)

Equations

• One or more equations did not get rendered due to their size.
• sys.kInduction 0 = pure ⟨k, sys⟩