def Esolangs.Cornucopia.OneAlt₁.exprOneAlt : Expr

Equations

• Esolangs.Cornucopia.OneAlt₁.exprOneAlt = Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.Expr.call "1" []], Esolangs.Cornucopia.Expr.call "1" []]

def Esolangs.Cornucopia.OneAlt₁.defOneAlt : Def

Equations

• Esolangs.Cornucopia.OneAlt₁.defOneAlt = { arity := 0, expr := Esolangs.Cornucopia.OneAlt₁.exprOneAlt }

def Esolangs.Cornucopia.OneAlt₁.defMain : Def

Equations

• Esolangs.Cornucopia.OneAlt₁.defMain = { arity := 1, expr := Esolangs.Cornucopia.Expr.call "1" [] }

def Esolangs.Cornucopia.OneAlt₁.defs : List (String × Def)

Equations

• Esolangs.Cornucopia.OneAlt₁.defs = [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.OneAlt₁.defMain), ("1", Esolangs.Cornucopia.OneAlt₁.defOneAlt)]

def Esolangs.Cornucopia.OneAlt₁.fs : List (String × (List ℕ → ℕ))

Equations

• Esolangs.Cornucopia.OneAlt₁.fs = [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.fn 1 fun (x : List ℕ) => 1), ("1", Esolangs.Cornucopia.fn 0 fun (x : List ℕ) => 1)]

def Esolangs.Cornucopia.OneAlt₁.fsMap : Map String (List ℕ → ℕ)

Equations

• Esolangs.Cornucopia.OneAlt₁.fsMap = Esolangs.Cornucopia.builtinFs ∪ Map.ofList Esolangs.Cornucopia.OneAlt₁.fs

def Esolangs.Cornucopia.OneAlt₁.prog : Prog

Equations

• Esolangs.Cornucopia.OneAlt₁.prog = Esolangs.Cornucopia.Prog.ofDefs Esolangs.Cornucopia.OneAlt₁.defs

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.nodup_defs : (List.map (fun (x : String × Def) => x.1) defs).Nodup

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.nodup_fs : (List.map (fun (x : String × (List ℕ → ℕ)) => x.1) fs).Nodup

@[simp]

instance Esolangs.Cornucopia.OneAlt₁.wfBuiltins_prog : prog.WFBuiltins

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.arity_oneAlt : defOneAlt.arity = 0

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.hasDef_prog_iff {name : String} : prog.HasDef name ↔ IsBuiltin name ∨ (defs.any fun (x : String × Def) => decide (x.1 = name)) = true

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.def?_oneAlt : prog.def? "1" = some defOneAlt

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.wfDefs' : WFDefs' defs

@[simp]

instance Esolangs.Cornucopia.OneAlt₁.wf' : prog.WF'

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.union_fs : builtinFs ∪ Map.ofList fs = fsMap

theorem Esolangs.Cornucopia.OneAlt₁.builtin_not_name_of_mem_fs {name₁ name : String} {d : List ℕ → ℕ} [H : BuiltinC name₁] (h : (name, d) ∈ fs) : name₁ ≠ name

theorem Esolangs.Cornucopia.OneAlt₁.get!_fsMap {name : String} : Map.get! name fsMap = match (motive := Option (String × (List ℕ → ℕ)) → List ℕ → ℕ) List.find? (fun (x : String × (List ℕ → ℕ)) => decide (x.1 = name)) fs with | some p => p.2 | none => Map.get! name builtinFs

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.not_builtin_mem_fs {name : String} {f : List ℕ → ℕ} [H : BuiltinC name] : (name, f) ∉ fs

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.get!_fsMap_builtin {name : String} [H : BuiltinC name] : Map.get! name fsMap = (BuiltinC.b name).eval

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.get!_fsMap_oneAlt : Map.get! "1" fsMap = fn 0 fun (x : List ℕ) => 1

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.compatibleDefs : CompatibleDefs (Map.ofList defs) (Map.ofList fs)

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.compatible : prog.Compatible fsMap

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get!_of {fs₁ : Map String (List ℕ → ℕ)} {name : String} (h : CompatibleDefs (Map.ofList defs) fs₁) (d : Def) (h₁ : (name, d) ∈ defs) (h₂ : ∀ (f : List ℕ → ℕ), Map.get! name (Map.ofList defs) = d → Map.get! name (builtinFs ∪ fs₁) = f → Map.get? name fs₁ = some (fn d.arity (d.expr.eval prog (builtinFs ∪ fs₁))) → Map.get? name fs₁ = some f → f = fn d.arity (d.expr.eval prog (builtinFs ∪ fs₁)) → fn d.arity f = Map.get! name (Map.ofList fs)) : Map.get! name (builtinFs ∪ fs₁) = Map.get! name (Map.ofList fs)

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.get!_defs_main : Map.get! mainName (Map.ofList defs) = defMain

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.get!_defs_oneAlt : Map.get! "1" (Map.ofList defs) = defOneAlt

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.get!_fs_main : Map.get! mainName (Map.ofList fs) = fn 1 fun (x : List ℕ) => 1

@[simp]

theorem Esolangs.Cornucopia.OneAlt₁.get!_fs_oneAlt : Map.get! "1" (Map.ofList fs) = fn 0 fun (x : List ℕ) => 1

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get?_builtin {fs₁ : Map String (List ℕ → ℕ)} {name : String} [H : BuiltinC name] (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? name (builtinFs ∪ fs₁) = some (BuiltinC.b name).eval

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get?_main {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? mainName fs₁ = some (fn 1 (defMain.expr.eval prog (builtinFs ∪ fs₁)))

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get?_oneAlt {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? "1" fs₁ = some (fn 0 (exprOneAlt.eval prog (builtinFs ∪ fs₁)))

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get!_builtin {fs₁ : Map String (List ℕ → ℕ)} {name : String} [H : BuiltinC name] (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get! name (builtinFs ∪ fs₁) = (BuiltinC.b name).eval

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get!_oneAlt {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get! "1" (builtinFs ∪ fs₁) = Map.get! "1" (Map.ofList fs)

theorem Esolangs.Cornucopia.OneAlt₁.fs₁_get!_main {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get! mainName (builtinFs ∪ fs₁) = Map.get! mainName (Map.ofList fs)

@[simp]

instance Esolangs.Cornucopia.OneAlt₁.wf_prog : prog.WF

@[instance_reducible]

instance Esolangs.Cornucopia.OneAlt₁.instProgInfoProg : ProgInfo prog

Equations

• Esolangs.Cornucopia.OneAlt₁.instProgInfoProg = { name := "OneAlt₁", defNames := ["main", "1"], has_model := true, has_unique_model := true, h_defNames := Esolangs.Cornucopia.OneAlt₁.instProgInfoProg._proof_1, h_wf' := Esolangs.Cornucopia.OneAlt₁.instProgInfoProg._proof_2, h_has_model := Esolangs.Cornucopia.OneAlt₁.instProgInfoProg._proof_3, h_has_unique_model := Esolangs.Cornucopia.OneAlt₁.instProgInfoProg._proof_4 }