View MemoOrdBinTree.v
Require Import Arith. | |
Require Import Omega. | |
Set Primitive Projections. | |
Set Implicit Arguments. | |
Inductive binTree : Set := | |
| Leaf : binTree | |
| Branch : binTree -> binTree -> binTree. |
View MemoBinTree.v
(* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *) | |
Require Import Vectors.Vector. | |
Import VectorNotations. | |
Set Primitive Projections. | |
Set Implicit Arguments. | |
Inductive binTree : Set := | |
| Leaf : binTree | |
| Branch : binTree -> binTree -> binTree. |
View ExtendedIncompletenessInQ0
// Define Computably Enumerable (aka recursively enumerable) predicates. | |
CESet : (Nat -> o) -> o | |
CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m) | |
// Standard Model | |
interpT : (Nat -> Nat) -> Term -> Nat | |
interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m) | |
interpF : (Nat -> Nat) -> Formula -> o |
View PatriciaTrie.v
Require Import Bvector. | |
Require Import Eqdep_dec. | |
Set Implicit Arguments. | |
Unset Strict Implicit. | |
Unset Printing Implicit Defensive. | |
Definition bCompare (x y : bool) : comparison := | |
match x, y with | |
| false, false => Eq |