def Esolangs.Cornucopia.Prog₁.defNot : Def

Equations

• Esolangs.Cornucopia.Prog₁.defNot = { arity := 1, expr := Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.one, Esolangs.Cornucopia.Expr.arg 0] }

def Esolangs.Cornucopia.Prog₁.defBool : Def

Equations

• Esolangs.Cornucopia.Prog₁.defBool = { arity := 1, expr := Esolangs.Cornucopia.Expr.call "not" [Esolangs.Cornucopia.Expr.call "not" [Esolangs.Cornucopia.Expr.arg 0]] }

def Esolangs.Cornucopia.Prog₁.exprAdd : Expr

Equations

• Esolangs.Cornucopia.Prog₁.exprAdd = Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.Expr.call "add" [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.arg 0, Esolangs.Cornucopia.one], Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.arg 1, Esolangs.Cornucopia.one]]]], Esolangs.Cornucopia.Expr.call "not" [Esolangs.Cornucopia.Expr.arg 0]], Esolangs.Cornucopia.Expr.call "not" [Esolangs.Cornucopia.Expr.arg 1]], Esolangs.Cornucopia.Expr.call "add" [Esolangs.Cornucopia.zero, Esolangs.Cornucopia.zero]]

def Esolangs.Cornucopia.Prog₁.defAdd : Def

Equations

• Esolangs.Cornucopia.Prog₁.defAdd = { arity := 2, expr := Esolangs.Cornucopia.Prog₁.exprAdd }

def Esolangs.Cornucopia.Prog₁.exprIte : Expr

Equations

• Esolangs.Cornucopia.Prog₁.exprIte = Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.succName [Esolangs.Cornucopia.Expr.call "ite" [Esolangs.Cornucopia.Expr.arg 0, Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.arg 1, Esolangs.Cornucopia.one], Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.arg 2, Esolangs.Cornucopia.one]]], Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call "bool" [Esolangs.Cornucopia.Expr.arg 0], Esolangs.Cornucopia.Expr.arg 1]], Esolangs.Cornucopia.Expr.call Esolangs.Cornucopia.subName [Esolangs.Cornucopia.Expr.call "not" [Esolangs.Cornucopia.Expr.arg 0], Esolangs.Cornucopia.Expr.arg 2]], Esolangs.Cornucopia.Expr.call "ite" [Esolangs.Cornucopia.Expr.arg 0, Esolangs.Cornucopia.zero, Esolangs.Cornucopia.zero]]

def Esolangs.Cornucopia.Prog₁.defIte : Def

Equations

• Esolangs.Cornucopia.Prog₁.defIte = { arity := 3, expr := Esolangs.Cornucopia.Prog₁.exprIte }

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

Equations

• Esolangs.Cornucopia.Prog₁.defs = [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.defId), ("0", Esolangs.Cornucopia.defZero), ("1", Esolangs.Cornucopia.defOne), ("not", Esolangs.Cornucopia.Prog₁.defNot), ("bool", Esolangs.Cornucopia.Prog₁.defBool), ("add", Esolangs.Cornucopia.Prog₁.defAdd), ("ite", Esolangs.Cornucopia.Prog₁.defIte)]

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

Equations

• Esolangs.Cornucopia.Prog₁.fs = [(Esolangs.Cornucopia.mainName, Esolangs.Cornucopia.fn 1 fun (x : List ℕ) => x[0]!), ("0", Esolangs.Cornucopia.fn 0 fun (x : List ℕ) => 0), ("1", Esolangs.Cornucopia.fn 0 fun (x : List ℕ) => 1), ("not", Esolangs.Cornucopia.fn 1 fun (xs : List ℕ) => if xs[0]! = 0 then 1 else 0), ("bool", Esolangs.Cornucopia.fn 1 fun (xs : List ℕ) => if xs[0]! = 0 then 0 else 1), ("add", Esolangs.Cornucopia.fn 2 fun (xs : List ℕ) => xs[0]! + xs[1]!), ("ite", Esolangs.Cornucopia.fn 3 fun (xs : List ℕ) => if xs[0]! = 0 then xs[2]! else xs[1]!)]

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

Equations

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

def Esolangs.Cornucopia.Prog₁.prog : Prog

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Esolangs.Cornucopia.Prog₁.arity_defNot : defNot.arity = 1

@[simp]

theorem Esolangs.Cornucopia.Prog₁.arity_defBool : defBool.arity = 1

@[simp]

theorem Esolangs.Cornucopia.Prog₁.arity_defAdd : defAdd.arity = 2

@[simp]

theorem Esolangs.Cornucopia.Prog₁.arity_defIte : defIte.arity = 3

@[simp]

theorem Esolangs.Cornucopia.Prog₁.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.Prog₁.def?_zero : prog.def? "0" = some defZero

@[simp]

theorem Esolangs.Cornucopia.Prog₁.def?_one : prog.def? "1" = some defOne

@[simp]

theorem Esolangs.Cornucopia.Prog₁.def?_not : prog.def? "not" = some defNot

@[simp]

theorem Esolangs.Cornucopia.Prog₁.def?_bool : prog.def? "bool" = some defBool

@[simp]

theorem Esolangs.Cornucopia.Prog₁.def?_add : prog.def? "add" = some defAdd

@[simp]

theorem Esolangs.Cornucopia.Prog₁.def?_ite : prog.def? "ite" = some defIte

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Esolangs.Cornucopia.Prog₁.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.Prog₁.not_builtin_mem_fs {name : String} {f : List ℕ → ℕ} [H : BuiltinC name] : (name, f) ∉ fs

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fsMap_not : Map.get! "not" fsMap = fn 1 fun (xs : List ℕ) => if xs[0]! = 0 then 1 else 0

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fsMap_bool : Map.get! "bool" fsMap = fn 1 fun (xs : List ℕ) => if xs[0]! = 0 then 0 else 1

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fsMap_add : Map.get! "add" fsMap = fn 2 fun (xs : List ℕ) => xs[0]! + xs[1]!

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fsMap_ite : Map.get! "ite" fsMap = fn 3 fun (xs : List ℕ) => if xs[0]! = 0 then xs[2]! else xs[1]!

@[simp]

theorem Esolangs.Cornucopia.Prog₁.eval_zero {xs : List ℕ} : zero.eval prog fsMap xs = 0

@[simp]

theorem Esolangs.Cornucopia.Prog₁.eval_one {xs : List ℕ} : one.eval prog fsMap xs = 1

@[simp]

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

@[simp]

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

theorem Esolangs.Cornucopia.Prog₁.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.Prog₁.get!_defs_main : Map.get! mainName (Map.ofList defs) = { arity := 1, expr := exprId }

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_defs_zero : Map.get! "0" (Map.ofList defs) = defZero

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_defs_one : Map.get! "1" (Map.ofList defs) = defOne

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_defs_not : Map.get! "not" (Map.ofList defs) = defNot

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_defs_bool : Map.get! "bool" (Map.ofList defs) = defBool

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_defs_add : Map.get! "add" (Map.ofList defs) = defAdd

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_defs_ite : Map.get! "ite" (Map.ofList defs) = defIte

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fs_not : Map.get! "not" (Map.ofList fs) = fn 1 fun (xs : List ℕ) => if xs[0]! = 0 then 1 else 0

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fs_bool : Map.get! "bool" (Map.ofList fs) = fn 1 fun (xs : List ℕ) => if xs[0]! = 0 then 0 else 1

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fs_add : Map.get! "add" (Map.ofList fs) = fn 2 fun (xs : List ℕ) => xs[0]! + xs[1]!

@[simp]

theorem Esolangs.Cornucopia.Prog₁.get!_fs_ite : Map.get! "ite" (Map.ofList fs) = fn 3 fun (xs : List ℕ) => if xs[0]! = 0 then xs[2]! else xs[1]!

theorem Esolangs.Cornucopia.Prog₁.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.Prog₁.fs₁_get?_main {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? mainName fs₁ = some (fn 1 (exprId.eval prog (builtinFs ∪ fs₁)))

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

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

theorem Esolangs.Cornucopia.Prog₁.fs₁_get?_not {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? "not" fs₁ = some (fn 1 (defNot.expr.eval prog (builtinFs ∪ fs₁)))

theorem Esolangs.Cornucopia.Prog₁.fs₁_get?_bool {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? "bool" fs₁ = some (fn 1 (defBool.expr.eval prog (builtinFs ∪ fs₁)))

theorem Esolangs.Cornucopia.Prog₁.fs₁_get?_add {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? "add" fs₁ = some (fn 2 (defAdd.expr.eval prog (builtinFs ∪ fs₁)))

theorem Esolangs.Cornucopia.Prog₁.fs₁_get?_ite {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get? "ite" fs₁ = some (fn 3 (defIte.expr.eval prog (builtinFs ∪ fs₁)))

theorem Esolangs.Cornucopia.Prog₁.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.Prog₁.fs₁_get!_main {fs₁ : Map String (List ℕ → ℕ)} (h : CompatibleDefs (Map.ofList defs) fs₁) : Map.get! mainName (builtinFs ∪ fs₁) = Map.get! mainName (Map.ofList fs)

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

theorem Esolangs.Cornucopia.Prog₁.fs₁_zero {fs₁ : Map String (List ℕ → ℕ)} {xs : List ℕ} (h : CompatibleDefs (Map.ofList defs) fs₁) : zero.eval prog (builtinFs ∪ fs₁) xs = 0

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

theorem Esolangs.Cornucopia.Prog₁.fs₁_one {fs₁ : Map String (List ℕ → ℕ)} {xs : List ℕ} (h : CompatibleDefs (Map.ofList defs) fs₁) : one.eval prog (builtinFs ∪ fs₁) xs = 1

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

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

theorem Esolangs.Cornucopia.Prog₁.exprAdd_aux (f : ℕ → ℕ → ℕ) (h : ∀ (x y : ℕ), f x y = ((f (x - 1) (y - 1) + 2 - if x = 0 then 1 else 0) - if y = 0 then 1 else 0) - f 0 0) : f = fun (x1 x2 : ℕ) => x1 + x2

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

theorem Esolangs.Cornucopia.Prog₁.exprIte_aux (f : ℕ → ℕ → ℕ → ℕ) (h : ∀ (a b c : ℕ), f a b c = f a (b - 1) (c - 1) + 1 - ((if a = 0 then 0 else 1) - b) - ((if a = 0 then 1 else 0) - c) - f a 0 0) : f = fun (a b c : ℕ) => if a = 0 then c else b

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

@[simp]

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

@[instance_reducible]

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

Equations

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