diff --git a/.gitignore b/.gitignore
index 9f318ed2a..2a01b1063 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,3 +19,6 @@ _scratch.egg
 
 # racket
 scripts/compiled
+semantics/compiled
+semantics/*.png
+docs
diff --git a/Makefile b/Makefile
index f67c3a881..43c97271b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: all web test nits docs serve graphs rm-graphs
+.PHONY: all web test nits docs serve graphs rm-graphs semantics
 
 RUST_SRC=$(shell find . -type f -wholename '*/src/*.rs' -or -name 'Cargo.toml')
 TESTS=$(shell find tests/ -type f -name '*.egg' -not -name '*repro-*')
@@ -10,7 +10,7 @@ WEB_SRC=$(wildcard web-demo/static/*)
 WASM=web_demo.js web_demo_bg.wasm
 DIST_WASM=$(addprefix ${WWW}, ${WASM})
 
-all: test nits web docs
+all: test nits web docs semantics
 
 test:
 	cargo nextest run --release
@@ -44,6 +44,11 @@ ${DIST_WASM}: ${RUST_SRC}
 	wasm-pack build web-demo --target no-modules --no-typescript --out-dir ${WWW}
 	rm -f ${WWW}/{.gitignore,package.json}
 
+semantics:
+	mkdir -p ./docs
+	scribble --dest ./docs semantics/*.scrbl
+	raco test semantics/*.rkt
+
 graphs: $(patsubst %.egg,%.svg,$(filter-out $(wildcard tests/repro-*.egg),$(wildcard tests/*.egg)))
 
 %.svg: %.egg
diff --git a/semantics/semantics.rkt b/semantics/semantics.rkt
new file mode 100644
index 000000000..b1484799f
--- /dev/null
+++ b/semantics/semantics.rkt
@@ -0,0 +1,710 @@
+#lang racket
+
+(require redex)
+(require pict)
+
+(provide (all-defined-out))
+
+
+;; here's how to set the style of everything
+;; for example, modern (monospace) style:
+#;((default-style 'modern)
+(grammar-style 'modern)
+(label-style 'modern)
+(paren-style 'modern)
+(literal-style (cons 'bold 'modern))
+(metafunction-style 'modern)
+(non-terminal-style 'modern)
+(non-terminal-subscript-style 'modern)
+(non-terminal-superscript-style 'modern))
+
+
+(define-language Egglog
+  [Program
+   (Cmd ...)]
+  [Cmd Action
+       Rule
+       (run) ;; TODO add schedules
+       skip]
+  [Rule
+    (rule Query Actions)]
+  [Query (Pattern ...)] ;; Query is a list of Pattern
+  [Pattern (= expr expr) ;; equality constraint
+           expr]
+  [Actions (Action ...)]
+  [Action expr
+          (let var expr)
+          (union expr expr)]
+  [expr number
+        (constructor expr ...)
+        var]
+  [constructor variable-not-otherwise-mentioned]
+  [var variable-not-otherwise-mentioned]
+  [ReservedSymbol -> :]) ;; variable-not-otherwise-mentioned needs to not use these since we use them in Database
+
+(define-extended-language
+  Egglog+Database
+  Egglog
+  ;; Egglog maintains a Database as global state.
+  ;; The database contains terms, a congruence
+  ;; closure over those terms,
+  ;; a set of global variable bindings,
+  ;; and a set of rules (only run by run commands).
+  ;; The environment is also used for
+  ;; local variable bindings when
+  ;; running rules.
+  [Database (Terms Congr Env Rules)]
+  [Congr
+   (congr Eq ...)]
+  [Eq
+   (= Term Term)]
+  [Terms
+   (tset Term ...)]
+  [Term number
+        (constructor Term ...)]
+  [Rules (Rule ...)]
+  [Command+Database
+   (Cmd Database)]
+  [Envs (Env ...)]
+  [Env (Binding ...)]
+  [Binding (var -> Term)]
+  [TypeEnv (TypeBinding ...)]
+  [TypeBinding (var : Type)]
+  ;; TODO add types- right now we just
+  ;; check there are no free variables
+  [Type no-type])
+
+(define-syntax-rule (rterm term)
+  (render-term Egglog+Database term))
+
+;; No rule for if the variable is not found
+;; Therefore it fails in such cases
+(define-metafunction Egglog+Database
+  Lookup : var Env -> Term ∨ #f
+  [(Lookup var_1 ())
+   #f]
+  [(Lookup var_1 ((var_1 -> Term_1) (var_s -> Term_s) ...))
+   Term_1]
+  [(Lookup var_1 ((var_2 -> Term_1) (var_s -> Term_s) ...))
+   (Lookup var_1 ((var_s -> Term_s) ...))
+   (side-condition (not (equal? (term var_1)
+                                (term var_2))))])
+
+
+(define-metafunction Egglog+Database
+  Dedup : Database -> Database
+  [(Dedup
+    ((tset Term_i ...)
+     (congr Eq_i ...)
+     (Binding_i ...)
+     (Rule_i ...)))
+   (,(cons 'tset (remove-duplicates (term (Term_i ...))))
+    ,(cons 'congr (remove-duplicates (term (Eq_i ...))))
+    ,(remove-duplicates (term (Binding_i ...)))
+    ,(remove-duplicates (term (Rule_i ...))))])
+
+(define-metafunction Egglog+Database
+  U_d : Database ... -> Database
+  [(U_d)
+   ((tset) (congr) () ())]
+  [(U_d ((tset Term_i ...) (congr Eq_i ...) (Binding_i ...) (Rule_i ...)) ...)
+   (Dedup ((tset Term_i ... ...) (congr Eq_i ... ...) (Binding_i ... ...) (Rule_i ... ...)))])
+
+
+(define-metafunction Egglog+Database
+ tset-union : Terms ... -> Terms
+ [(tset-union (tset Term_i ...) ...)
+  ,(cons 'tset (remove-duplicates (term (Term_i ... ...))))])
+
+(define-metafunction Egglog+Database
+ congr-union : Congr ... -> Congr
+ [(congr-union (congr Eq_i ...) ...)
+  ,(cons 'congr (remove-duplicates (term (Eq_i ... ...))))])
+
+(define-metafunction Egglog+Database
+  tset-not-in : Term Terms -> #t ∨ #f
+  [(tset-not-in Term_1 (tset Term_2 ...))
+   #t
+   (side-condition
+    (not (member (term Term_1)
+                 (term (Term_2 ...)))))]
+  [(tset-not-in Term_1 (tset Term_2 ...))
+    #f
+    (side-condition
+      (member (term Term_1)
+              (term (Term_2 ...))))])
+
+(define-judgment-form Egglog+Database
+  #:contract (tset-element Term Terms)
+  #:mode (tset-element O I)
+  [----------------------
+   (tset-element Term_a (tset Term_i ... Term_a Term_j ...))])
+
+(define-judgment-form Egglog+Database
+  #:contract (congr-element Eq Congr)
+  #:mode (congr-element O I)
+  [----------------------
+   (congr-element Eq_res (congr Eq_i ... Eq_res Eq_j ...))])
+
+(define-metafunction Egglog+Database
+  tset-subtract : Terms Terms -> Terms
+  [(tset-subtract Terms (tset))
+   Terms]
+  [(tset-subtract (tset Term_i ...) (tset Term_a Term_j ...))
+   (tset-subtract
+     ,(cons 'tset (remove (term Term_a) (term (Term_i ...))))
+     (tset Term_j ...))])
+
+(define-metafunction Egglog+Database
+  Eval-Expr : expr Env -> Term
+  [(Eval-Expr number Env)
+   number]
+  [(Eval-Expr var Env)
+   (Lookup var Env)]
+  [(Eval-Expr (constructor expr_s ...) Env)
+   (constructor (Eval-Expr expr_s Env) ...)])
+
+
+(define (dump-pict pict name)
+  (send (pict->bitmap pict)
+        save-file
+        name
+        'png))
+
+(define-metafunction Egglog+Database
+  Eval-Action : Action Database -> Database
+  [(Eval-Action (let var expr) (Terms Congr (Binding_s ...) Rules_1))
+   ((tset-union (tset Term_res) Terms) Congr ((var -> Term_res) Binding_s ...) Rules_1)
+   (where Term_res
+          (Eval-Expr expr (Binding_s ...)))]
+  [(Eval-Action expr (Terms Congr Env Rules_1))
+   ((tset-union (tset Term_res) Terms) Congr Env Rules_1)
+   (where Term_res (Eval-Expr expr Env))]
+  [(Eval-Action (union expr_1 expr_2) (Terms_1 (congr Eq ...) Env_1 Rules_1))
+   ((tset-union (tset Term_1 Term_2) Terms_1) (congr (= Term_1 Term_2) Eq ...) Env_1 Rules_1)
+   (where Term_1 (Eval-Expr expr_1 Env_1))
+   (where Term_2 (Eval-Expr expr_2 Env_1))])
+
+
+
+
+(define-metafunction
+  Egglog+Database
+  congr-subset : Congr Congr -> #t ∨ #f
+  [(congr-subset (congr) (congr Eq_i ...))
+   #t]
+  [(congr-subset (congr Eq_1 Eq_i ...) (congr Eq_j ... Eq_1 Eq_k ...))
+   (congr-subset (congr Eq_i ...) (congr Eq_j ... Eq_1 Eq_k ...))]
+  [(congr-subset (congr Eq_1 Eq_i ...) (congr Eq_j ...))
+   #f
+   (side-condition
+    (not (member (term Eq_1) (term (Eq_j ...)))))])
+
+(define-metafunction
+  Egglog+Database
+  tset-subset : Terms Terms -> #t ∨ #f
+  [(tset-subset (tset Term_i ...) (tset Term_j ...))
+   ,(subset? (list->set (term (Term_i ...)))
+             (list->set (term (Term_j ...))))])
+
+;; A reduction relation that restores the congruence
+;; relation after some equalities have been added
+(define Congruence-Reduction
+  (reduction-relation
+   Egglog+Database
+   #:domain Database
+   (-->
+    (Terms Congr Env Rules_1)
+    (Terms (congr-union (congr (= Term_i Term_i)) Congr) Env Rules_1)
+    (judgment-holds (tset-element Term_i Terms))
+    (side-condition/hidden ;; side condition so redex terminates
+     (not
+      (member (term (= Term_i Term_i))
+              (term Congr))))
+    "reflexivity")
+   (-->
+    (Terms Congr Env Rules_1)
+    (Terms (congr-union (congr (= Term_2 Term_1)) Congr) Env Rules_1)
+    (judgment-holds (congr-element (= Term_1 Term_2) Congr))
+    (side-condition/hidden
+     (not
+      (member (term (= Term_2 Term_1))
+              (term Congr))))
+    "symmetry"
+    )
+   (-->
+    (Terms Congr Env Rules_1)
+    (Terms (congr-union (congr (= Term_1 Term_3)) Congr) Env Rules_1)
+    (judgment-holds (congr-element (= Term_1 Term_2) Congr))
+    (judgment-holds (congr-element (= Term_2 Term_3) Congr))
+    (side-condition/hidden
+     (not
+      (member (term (= Term_1 Term_3))
+              (term Congr))))
+    "transitivity"
+    )
+   (-->
+    (Terms Congr Env Rules_1)
+    (Terms (congr-union (congr (= (constructor_1 Term_i ...) (constructor_1 Term_j ...))) Congr) Env Rules_1)
+    (judgment-holds (tset-element (constructor_1 Term_i ..._1) Terms))
+    (judgment-holds (tset-element (constructor_1 Term_j ..._1) Terms))
+    (side-condition (term (congr-subset (congr (= Term_i Term_j) ...) Congr)))
+    (side-condition/hidden
+     (not
+      (member (term (= (constructor_1 Term_i ...)
+                       (constructor_1 Term_j ...)))
+              (term Congr))))
+    "congruence"
+    )
+   (-->
+    (Terms Congr Env Rules)
+    ((tset-union (tset Term_c) Terms) Congr Env Rules)
+    (judgment-holds
+     (tset-element (constructor Term_i ... Term_c Term_j ...) Terms))
+    (side-condition/hidden
+     (not (member (term Term_c) (term Terms))))
+    "presence of children"
+     )
+    ))
+
+;; Like apply-reduction-relation*, but only
+;; returns the first path found.
+;; Instead of returning a list, it returns
+;; a single term.
+(define (apply-reduction-relation-one-path relation term)
+  (match (apply-reduction-relation relation term)
+    [`(,reduced ,others ...)
+     (apply-reduction-relation-one-path relation reduced)]
+    [`()
+     term]))
+
+(define-metafunction
+  Egglog+Database
+  restore-congruence : Database -> Database
+  [(restore-congruence Database)
+   ,(apply-reduction-relation-one-path Congruence-Reduction (term Database))])
+
+(define-metafunction
+  Egglog+Database
+  Eval-Global-Actions : Actions Database -> Database
+  [(Eval-Global-Actions () Database)
+   Database]
+  [(Eval-Global-Actions (Action_1 Action_i ...) Database_1)
+   (Eval-Global-Actions (Action_i ...) (Eval-Action Action_1 Database_1))])
+
+(define-metafunction
+  Egglog+Database
+  Eval-Local-Actions : Actions Database Env -> Database
+  [(Eval-Local-Actions Actions Database_1 Env_local)
+   (Terms_2 Congr_2 Env_1 Rules_1)
+   (where (Terms_1 Congr_1 Env_1 Rules_1) Database_1)
+   (where (Terms_2 Congr_2 Env_2 Rules_2)
+          ;; all on the same line for typesetting
+          (Eval-Global-Actions Actions (Terms_1 Congr_1 (Env-Union Env_1 Env_local) Rules_1)))])
+                           
+  
+
+(define-metafunction
+  Egglog+Database
+  Eval-Actions : Rule Database Envs -> Database
+  [(Eval-Actions (rule Query Actions) Database (Env_i ...))
+   (U_d (Eval-Local-Actions Actions Database Env_i) ...)])
+
+(define-metafunction Egglog+Database
+  unbound : var Env -> #t ∨ #f
+  [(unbound var_1 Env)
+   ,(not (member (term var_1)
+                 (map first (term Env))))])
+
+;; Appends some environments, and returns
+;; #f if they are incompatible
+(define-metafunction
+  Egglog+Database
+  Env-Union : Env ... -> Env ∨ #f
+  [(Env-Union)
+   ()]
+  [(Env-Union Env)
+   Env]
+  [(Env-Union Env_1 Env_2 Env_i ...)
+   (Env-Union Env_r Env_i ...)
+   (where Env_r (Env-Union2 Env_1 Env_2))]
+  [(Env-Union Env_1 Env_2 Env_i ...)
+   #f
+   (where #f (Env-Union2 Env_1 Env_2))])
+
+;; Appends two environments.
+;; Returns #f if they are incompatible.
+(define-metafunction
+  Egglog+Database
+  Env-Union2 : Env Env -> Env ∨ #f
+  [(Env-Union2 () Env)
+   Env]
+  [(Env-Union2 ((var -> Term) Binding_i ...) Env)
+   ((var -> Term) Binding_r ...)
+   (where (Binding_r ...)
+          (Env-Union2 (Binding_i ...) Env))
+   (side-condition
+    (or (equal? (term (Lookup var Env))
+                (term Term))
+        (term (unbound var Env))))]
+  [(Env-Union2 ((var -> Term) Binding_i ...) Env)
+   #f
+   (side-condition
+     (not (or (equal? (term (Lookup var Env))
+                      (term Term))
+              (term (unbound var Env)))))])
+
+(define-metafunction
+  Egglog+Database
+  varset-union : (var ...) ... -> (var ...)
+  [(varset-union (var_i ...) ...)
+   ,(remove-duplicates (term (var_i ... ...)))])
+
+(define-metafunction
+  Egglog+Database
+  vars-union : (var ...) ... -> (var ...)
+  [(vars-union (var_i ...) ...)
+   ,(remove-duplicates (term (var_i ... ...)))])
+
+(define-metafunction
+  Egglog+Database
+  free-vars : expr Env -> (var ...)
+  [(free-vars number Env)
+   ()]
+  [(free-vars (constructor expr_i ...) Env)
+   (varset-union (free-vars expr_i Env) ...)]
+  [(free-vars var Env)
+   (var)
+   (where #t (unbound var Env))]
+  [(free-vars var Env)
+   ()
+   (where #f (unbound var Env))])
+
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (tset-is-subset Terms Terms)
+  #:mode (tset-is-subset O I)
+  [(tset-is-subset-helper Terms_1 Terms_2 (tset))
+   -----------------------------------------
+   (tset-is-subset Terms_1 Terms_2)])
+
+;; Finds all subsets of a set
+;; Uses a third set, which is initially empty
+;; The third set prevents re-adding elements
+;; and allows redex to terminate
+;; Warning: judgement is extremely slow to execute
+(define-judgment-form
+  Egglog+Database
+  #:contract (tset-is-subset-helper Terms Terms Terms)
+  #:mode (tset-is-subset-helper O I I)
+  [------------------------------
+   (tset-is-subset-helper (tset) Terms_2 Terms_3)]
+  [(tset-element Term_a Terms_2)
+   (where #t (tset-not-in Term_a Terms_3))
+   (tset-is-subset-helper Terms_1 Terms_2
+                   (tset-union Terms_3 (tset Term_a)))
+   ------------------------------
+   (tset-is-subset-helper (tset-union Terms_1 (tset Term_a)) Terms_2 Terms_3)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (valid-env (var ...) Database Env)
+  #:mode (valid-env I I O)
+  [(tset-is-subset (tset Term_i ..._1) Terms_1)
+   -------------------------------------
+   (valid-env (var_i ..._1) (Terms_1 Congr_1 Env_1 Rules_1) ((var_i -> Term_i) ...))])
+
+
+;; Defines e-matching in terms of matching a
+;; witness term.
+;; A valid substitution satisfies:
+;; - is an assignment of variables to terms that are in the database
+;; - when the pattern is evaluated in the database, the resulting term is equal to some witness term
+;; - the witness term is in the original database
+(define-judgment-form
+  Egglog+Database
+  #:contract (valid-subst Database Pattern Env)
+  #:mode (valid-subst I I O)
+  [(where (Terms_1 Congr_1 Env_1 Rules_1)
+          Database_1)
+   (valid-env (free-vars expr Env_1) Database_1 Env_subst)
+   (tset-element Term_witness Terms_1)
+   (where Term_res (Eval-Expr expr (Env-Union Env_1 Env_subst)))
+   (where (Terms_2 Congr_2 Env_2 Rules_2)
+          (restore-congruence (U_d Database_1 ((tset Term_res) (congr) () ()))))
+   (side-condition
+     (congr-subset (congr (= Term_witness Term_res)) Congr_2))
+   --------------------------------------
+   (valid-subst Database_1 expr Env_subst)]
+  [(where (Terms_1 Congr_1 Env_1 Rules_1) Database_1)
+   (valid-env (vars-union (free-vars expr_1 Env_1) (free-vars expr_2 Env_1)) Database_1 Env_subst)
+   (tset-element Term_witness Terms_1)
+   (where Term_res1
+          (Eval-Expr expr_1
+            (Env-Union Env_1 Env_subst)))
+   (where Term_res2
+          (Eval-Expr expr_2
+            (Env-Union Env_1 Env_subst)))
+   (where (Terms_2 Congr_2 Env_2 Rules_2)
+          (restore-congruence (U_d Database_1 ((tset Term_res1 Term_res2) (congr) () ()))))
+   (side-condition (congr-subset (congr (= Term_witness Term_res1) (= Term_res1 Term_res2)) Congr_2))
+   -------------------------------------
+   (valid-subst Database_1 (= expr_1 expr_2) Env_subst)]
+   )
+
+
+;; Experimental alternate semantics for valid-subst
+;; that is probably much faster to run with redex
+;; For a database, pattern, term, and environment,
+;; valid-subst-faster judges that the pattern e-matches
+;; the witness term with local substitution given by the environment.
+;; `valid-subst-faster` defines e-matching by specifying
+;; which environments satisfy a query.
+(define-judgment-form
+  Egglog+Database
+  #:contract (valid-subst-faster Database Pattern Term Env)
+  #:mode (valid-subst-faster I I O O)
+  [(where #t (unbound var Env))
+   ----------------------------
+   (valid-subst-faster ((tset Term_i ... Term_1 Term_j ...) Congr Env Rules)
+                var
+                Term_1
+                ((var -> Term_1)))]
+  [-----------------------------
+   (valid-subst-faster
+    (Terms Congr (Binding_i ... (var -> Term_1) Binding_j ...) Rules)
+    var
+    Term_1
+    ())]
+  [-----------------------------
+   (valid-subst-faster Database number number ())]
+  [(valid-subst-faster Database Pattern_i Term_i Env_i) ...
+   (where ((tset Term_x ... 
+     (constructor Term_j ...)
+     Term_z ...) Congr Env Rules) Database)
+   (where #t (congr-subset (congr (= Term_i Term_j) ...) Congr))
+   (where Env_r (Env-Union Env_i ...))
+   -----------------------------
+   (valid-subst-faster
+    Database
+    (constructor Pattern_i ...)
+    (constructor Term_j ...)
+    Env_r)])
+
+
+;; If a local environment is valid
+;; for a set of patterns, it is valid for
+;; the overall query.
+(define-judgment-form
+  Egglog+Database
+  #:contract (valid-query-subst Database Query Env)
+  #:mode (valid-query-subst I I O)
+  [(valid-subst Database Pattern_i Env_i) ...
+   (where Env_r (Env-Union Env_i ...))
+   ---------------------------
+   (valid-query-subst Database (Pattern_i ...) Env_r)])
+
+
+(define-metafunction
+  Egglog+Database
+  all-valid-query-subst : Database Query -> Envs
+  [(all-valid-query-subst Database Query)
+   ,(judgment-holds (valid-query-subst Database Query Env) Env)])
+
+;; Performs the rule's query, returning a set
+;; of environments that satisfy the query
+(define-metafunction
+  Egglog+Database
+  Rule-Envs : Database Rule -> Envs
+  [(Rule-Envs Database (rule Query Actions))
+   ;; Perform e-matching using redex
+   (all-valid-query-subst Database Query)])
+
+(define -->_Command (rterm -->_Command))
+(set-arrow-pict! '-->_Command
+ (lambda () -->_Command))
+(define Command-Reduction
+  (reduction-relation
+   Egglog+Database
+   #:domain Command+Database
+   #:arrow -->_Command
+   ;; running actions
+   (-->_Command
+    (Action Database)
+    (skip (Eval-Action Action Database)))
+   (-->_Command
+    (Rule (Terms Congr Env (Rule_i ...)))
+    (skip (Terms Congr Env (Rule Rule_i ...))))
+   (-->_Command
+    ((run) Database)
+    (skip (U_d Database Database_i ...))
+    (where (Terms Congr Env (Rule ...))
+           Database)
+    (where (Envs ...)
+           ((Rule-Envs Database Rule) ...))
+    (where (Database_i ...)
+           ((Eval-Actions Rule Database Envs) ...)))))
+
+
+(define (try-apply-reduction-relation relation term)
+  (define lst (apply-reduction-relation relation term))
+  (match lst
+    [`(,x) x]
+    [`() #f]
+    [_ (error "Expected single element, got ~a" lst)]))
+
+
+(define -->_Program (rterm -->_Program))
+(set-arrow-pict! '-->_Program
+ (lambda () -->_Program))
+(define Egglog-Reduction
+  (reduction-relation
+   Egglog+Database
+   #:domain (Program Database)
+   #:arrow -->_Program
+   (-->_Program
+    ((Cmd_1 Cmd_s ...) Database)
+    ((Cmd_s ...) (restore-congruence Database_2))
+    (where/hidden ;; hide this from typesetting
+     (skip Database_2)
+     ,(try-apply-reduction-relation
+       Command-Reduction
+       (term (Cmd_1 Database))))
+    (side-condition #t) ;; use this instead)
+  )))
+
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-expr expr TypeEnv)
+  #:mode (typed-expr I I)
+  [----------------------------
+   (typed-expr number TypeEnv)]
+  [(side-condition ,(member (term (var : no-type))
+                            (term TypeEnv)))
+   ----------------------------
+   (typed-expr var TypeEnv)]
+  [(typed-expr expr_s TypeEnv) ...
+   ----------------------------
+   (typed-expr (constructor expr_s ...) TypeEnv)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-query-expr expr TypeEnv TypeEnv)
+  #:mode (typed-query-expr I I O)
+  [----------------------------
+   (typed-query-expr number TypeEnv TypeEnv)]
+  ;; no need to add it, refers to global
+  ;; or previously defined
+  [(side-condition ,(member (term (var : no-type))
+                            (term TypeEnv)))
+   ----------------------------
+   (typed-query-expr var TypeEnv TypeEnv)]
+  ;; add it to environment if not bound 
+  [(side-condition ,(not
+                     (member (term
+                              (var : no-type))
+                             (term
+                              (TypeBinding ...)))))
+   ----------------------------
+   (typed-query-expr var
+                     (TypeBinding ...)
+                     ((var : no-type)
+                      TypeBinding ...))]
+  [(typed-query-expr expr_s TypeEnv (TypeBinding ...)) ...
+   ----------------------------
+   (typed-query-expr
+    (constructor expr_s ...)
+    TypeEnv
+    (TypeBinding ... ...))])
+
+
+(define-judgment-form
+  Egglog+Database
+  ;; Types an Action in a given environment and
+  ;; returns the resulting environment
+  #:contract (typed-action Action TypeEnv TypeEnv)
+  #:mode (typed-action I I O)
+  [(side-condition ,(not
+                     (member
+                      (term (TypeBinding ...))
+                      (term (TypeBinding ...)))))
+   (typed-expr expr (TypeBinding ...))
+   ----------------------------
+   (typed-action (let var expr)
+                 (TypeBinding ...)
+                 ((var : no-type)
+                  TypeBinding ...))]
+  [(typed-expr expr TypeEnv)
+   ----------------------------
+   (typed-action expr TypeEnv TypeEnv)]
+  [(typed-expr expr_1 TypeEnv)
+   (typed-expr expr_2 TypeEnv)
+   ----------------------------
+   (typed-action (union expr_1 expr_2) TypeEnv TypeEnv)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-pattern Pattern TypeEnv TypeEnv)
+  #:mode (typed-pattern I I O)
+  [(typed-query-expr expr TypeEnv TypeEnv_2)
+    ----------------------------
+   (typed-pattern expr TypeEnv TypeEnv_2)]
+  [(typed-query-expr expr_1 TypeEnv TypeEnv_2)
+   (typed-query-expr expr_2 TypeEnv_2 TypeEnv_3)
+   ----------------------------
+   (typed-pattern (= expr_1 expr_2)
+                  TypeEnv TypeEnv_3)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-query Query TypeEnv TypeEnv)
+  #:mode (typed-query I I O)
+  [------------------------
+   (typed-query () TypeEnv TypeEnv)]
+  [(typed-query (Pattern_i ...) TypeEnv TypeEnv_2)
+   (typed-pattern Pattern TypeEnv_2 TypeEnv_3)
+   ------------------------
+   (typed-query (Pattern_i ... Pattern) TypeEnv TypeEnv_3)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-actions Actions TypeEnv TypeEnv)
+  #:mode (typed-actions I I O)
+  [------------------------
+   (typed-actions () TypeEnv TypeEnv)]
+  [(typed-actions (Action_i ...) TypeEnv TypeEnv_2)
+   (typed-action Action TypeEnv_2 TypeEnv_3)
+   ------------------------
+   (typed-actions
+    (Action_i ... Action)
+    TypeEnv TypeEnv_3)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-rule Rule TypeEnv)
+  #:mode (typed-rule I I)
+  [(typed-query Query TypeEnv TypeEnv_2)
+   (typed-actions Actions TypeEnv_2 TypeEnv_3)
+   ----------------------------
+   (typed-rule (rule Query Actions) TypeEnv)])
+
+(define-judgment-form
+  Egglog+Database
+  #:contract (typed-program Program TypeEnv)
+  #:mode (typed-program I O)
+  [---------------------------
+   (typed-program () ())]
+  [(typed-program (Cmd_p ...) TypeEnv)
+   (typed-action Action TypeEnv TypeEnv_res)
+   ---------------------------
+   (typed-program (Cmd_p ... Action) TypeEnv_res)]
+  [(typed-program (Cmd_p ...) TypeEnv)
+   (typed-rule Rule TypeEnv)
+   ---------------------------
+   (typed-program (Cmd_p ... Rule) TypeEnv)]
+  [(typed-program (Cmd_p ...) TypeEnv)
+   ---------------------------
+   (typed-program (Cmd_p ... (run)) TypeEnv)])
+
diff --git a/semantics/semantics.scrbl b/semantics/semantics.scrbl
new file mode 100644
index 000000000..db2f253e6
--- /dev/null
+++ b/semantics/semantics.scrbl
@@ -0,0 +1,305 @@
+#lang scribble/manual
+
+@(require racket/match)
+@(require scribble-math/dollar redex)
+@(require "semantics.rkt")
+@(require (except-in pict table))
+@(require scribble/core
+          scribble/html-properties
+          racket/runtime-path
+          (only-in xml cdata))
+
+@(define head-google
+  (head-extra (cdata #f #f "<link rel=\"stylesheet\"
+          href=\"https://fonts.googleapis.com/css?family=Nunito+Sa
+          ns\">")))
+
+@(define-runtime-path css-path "style.css")
+@(define css-object (css-addition css-path))
+
+@(define html5-style
+   (with-html5 manual-doc-style))
+@(define title-style
+   (struct-copy style html5-style
+                [properties
+                 (append
+                  (style-properties html5-style)
+                  (list css-object head-google))]))
+
+@(reduction-relation-rule-separation 10)
+@(metafunction-rule-gap-space 10)
+@(non-terminal-gap-space 10) 
+
+@(define (set-notation lws)
+  (match lws
+    [`(,paren ,tset ,elements ... ,paren2)
+      (append  `("" "{")
+                (if (equal? (length elements) 0)
+                    (list
+                    (struct-copy lw tset
+                      [e (blank)]))
+                    (list))
+                elements
+                `("}" ""))]
+    [else (error "bad tset")]))
+
+@(define (add-between lst element)
+   (apply append
+    (for/list ([ele lst]
+               [i (in-range (length lst))])
+      (if (zero? i)
+          (list ele)
+          (list element ele)))))
+
+@(define (set-union-notation lws)
+  (match lws
+    [`(,paren ,func-call ,elements ... ,paren2)
+      (append `("") (add-between elements "∪") `(""))]))
+
+@(define (set-element-notation lws)
+  (match lws
+    [`(,paren ,func-call ,element1 ,element2 ,paren2)
+      `("" ,element1 " ∈ " ,element2 "")]))
+
+@(define (set-subset-notation lws)
+  (match lws
+    [`(,paren ,func-call ,element1 ,element2 ,paren2)
+      `("" ,element1 " ⊆ " ,element2 "")]))
+
+@(define (my-render-reduction-relation reduction-relation)
+  (render
+   (lambda ()
+    (render-reduction-relation reduction-relation))))
+
+@(define (my-render-language language)
+  (render
+   (lambda ()
+    (render-language language))))
+
+@(define-syntax-rule (my-render-judgement judgement)
+  (render
+   (lambda ()
+    (render-judgment-form judgement))))
+
+@(define (all-valid-query-subst-notation lws)
+  (match lws
+    [`(,paren ,func-call ,elements ... ,paren2)
+      (append 
+        `("" "{Env s.t. (valid-query-subst ")
+         elements
+         `(" Env)}" ""))]))
+
+@(define-syntax-rule (my-render-metafunction metafunction)
+  (render
+   (lambda ()
+    (render-metafunction metafunction))))
+
+@(define (render func)
+  (parameterize ([rule-pict-style 'compact-vertical]
+                 [metafunction-pict-style 'left-right/vertical-side-conditions]
+                 [metafunction-fill-acceptable-width 10])
+    (with-compound-rewriters
+     (['tset set-notation]
+      ['congr set-notation]
+      ['vars-union set-union-notation]
+      ['tset-union set-union-notation]
+      ['congr-union set-union-notation]
+      ['tset-element set-element-notation]
+      ['congr-element set-element-notation]
+      ['tset-is-subset set-subset-notation]
+      ['congr-subset set-subset-notation]
+      ['all-valid-query-subst all-valid-query-subst-notation])
+     (func))))
+
+
+@title[#:style  title-style]{ Egglog Semantics }
+
+@section{Egglog Grammar}
+
+@(parameterize ([render-language-nts (remove 'ReservedSymbol (language-nts Egglog))])
+  (my-render-language Egglog))
+
+An egglog @code{Program} is a sequence of top-level @code{Cmd}s.
+Egglog keeps track of a global @code{Database}
+as it runs.
+An @code{Action} adds directly to the database.
+A @code{Rule} is added to the list of rules,
+and a @code{(run)} statement runs the rules.
+
+Rules have two parts: a @code{Query} and @code{Actions}.
+The @code{Query} is a set of patterns that must
+match terms in the database for the rule to fire.
+The @code{Actions} add to the database for every valid match.
+
+@;; don't include stuff about typechecking
+@;; since we don't do it yet
+@(parameterize ([render-language-nts
+                (remove* `(Type TypeEnv TypeBinding) (language-nts Egglog+Database))])
+  (my-render-language Egglog+Database))
+
+Egglog's global state is a @code{Database}, containing:
+@itemlist[
+ @item{A set of @code{Terms}}
+ @item{A set of equalities @code{Congr}, which forms a congruence closure}
+ @item{A set of global bindings @code{Env}}
+ @item{A set of rules @code{Rules}, which are run when @code{(run)} is called}
+]
+
+Running an @code{Action} may add terms and equalities to the database.
+In-between each command, the congruence closure over these terms is completed.
+
+@section{Running Commands}
+
+Egglog's top-level reduction relation @-->_Program runs a sequence of commands.
+Notice that between running commands, egglog restores the congruence relation (see section on restoring congruence).
+
+@(define stepped
+  (hc-append 10
+   (render-term Egglog
+    (Cmd_1 Database_1))
+   -->_Command
+   (render-term Egglog
+    (Cmd_stepped Database_2))))
+    
+@(with-unquote-rewriter
+  (lambda (old)
+    (struct-copy lw old
+      [e stepped]))
+  (my-render-reduction-relation Egglog-Reduction))
+
+The @-->_Command reduction relation defines
+how each of these commands is run.
+
+@(my-render-reduction-relation Command-Reduction)
+
+The next two sections will cover evaluating actions (@code{Eval-Actions}) and evaluating
+queries (@code{Rule-Envs}).
+
+@section{Evaluating Actions}
+
+Given an evironment @code{Env}, egglog's
+expressions construct a single term.
+The @code{Lookup} function looks up a term
+in the environment, given the variable.
+
+@(my-render-metafunction Eval-Expr)
+
+Egglog's actions add new terms and equalities to
+the global database.
+An action is either a let binding,
+an expression,
+or a union between two expressions.
+At the top level, let bindings add new global
+variables to the environment.
+In the actions of a rule, let bindings add
+new local variables.
+
+The resulting database after evaluating expressions may not contain all intermediate terms.
+These are added when the congruence closure
+is restored.
+
+@(my-render-metafunction Eval-Action)
+
+
+Evaluating a sequence of actions is done
+by evaluating each action in turn.
+Since actions only add terms to the set of terms
+and equalities to the congruence relation,
+the order of evaluation of these actions
+does not matter (besides needing variables to be bound first).
+
+@(my-render-metafunction Eval-Global-Actions)
+
+In order to evaluate local actions for
+a rule, we evaluate the actions in the global
+scope, then forget the resulting environment.
+
+@(my-render-metafunction Eval-Local-Actions)
+
+Given a set of substitutions from running a rule's query, we can evaluate
+a rule's actions by applying the actions 
+multiple times, once for each substitution.
+
+@(my-render-metafunction Eval-Actions)
+
+The @(rterm U_d) function is a database-union function. It takes two databases and unions the terms, equalities, environments, and rules.
+
+@(my-render-metafunction U_d)
+
+The @(rterm Dedup) metafunction removes duplicates from sets.
+
+@section{Evaluating Queries}
+
+To evaluate a rule, egglog first finds
+all valid substitutions for the rule's @code{Query}.
+
+@(my-render-metafunction Rule-Envs)
+
+The @code{valid-query-subst} judgement defines
+which environments (also called substitutions) are valid for a query.
+An environment @(rterm Env_r) is valid for a query if it is valid for each pattern in the query.
+The @(rterm Env-Union) metafunction ensures that the environments for each
+pattern are compatible: if they share variable
+bindings, they must be bound to the same term.
+
+
+@(my-render-judgement valid-query-subst)
+
+
+The @code{valid-subst} judgement defines
+when a substitution is valid for a pattern.
+It states these conditions:
+
+@itemlist[
+  @item{@(rterm Env_subst) is a valid environment mapping free variables in the pattern to grounded terms in the database}
+  @item{There exists a witness term @(rterm Term_witness) in the database}
+  @item{Evaluating the pattern with the substitution results in another term @(rterm Term_res)}
+  @item{@(rterm Term_res) is equal to @(rterm Term_witness) using the congruence closure.}
+]
+
+We say that the pattern and substitution `e-matches` the witness term.
+
+@(my-render-judgement valid-subst)
+
+@(rterm free-vars) returns the set of free variables of a pattern.
+Valid-env defines the set of valid environments
+mapping free variables to grounded terms.
+
+@(my-render-judgement valid-env)
+
+
+
+@section{Restoring Congruence}
+
+In-between every command, egglog restores
+the congruence closure using
+the axioms of congruence closure.
+It also uses a a "presence of children" axiom to ensure
+all terms, including their children, are present
+in the congruence closure.
+
+
+@(my-render-reduction-relation Congruence-Reduction)
+
+The restore-congruence metafunction applies
+the Congruence-Reduction until a fixed point.
+
+
+@section{To Do}
+
+This semantics is not yet complete, and does not
+cover everything egglog can do.
+
+
+@itemlist[
+ @item{Type checking: egglog enforces well-typed terms and rules, and supports
+ primitives}
+ @item{Seminaive evaluation: Egglog doesn't actually return all valid substitutions. Actully, it only returns new ones.}
+ @item{Merge functions: egglog supports merge
+ functions, which are a functional depedency from inputs to a single output.}
+ @item{Schedules: egglog supports running
+ different rulesets in a schedule}
+ @item{Extraction: egglog supports extracting
+ programs from the database}
+ @item{Containers: Egglog supports custom containers, such as vectors}
+]
\ No newline at end of file
diff --git a/semantics/style.css b/semantics/style.css
new file mode 100644
index 000000000..4248a7fc5
--- /dev/null
+++ b/semantics/style.css
@@ -0,0 +1,16 @@
+/* common to both blog and main page */
+body {
+  font-family: 'Nunito Sans', sans-serif;
+}
+
+p {
+  font-family: 'Nunito Sans', sans-serif;
+}
+
+div {
+  font-family: 'Nunito Sans', sans-serif;
+}
+
+html {
+  scroll-behavior: smooth;
+}
\ No newline at end of file
diff --git a/semantics/test.rkt b/semantics/test.rkt
new file mode 100644
index 000000000..6f5c67a90
--- /dev/null
+++ b/semantics/test.rkt
@@ -0,0 +1,347 @@
+#lang racket
+
+(require redex)
+(require rackunit)
+(require "semantics.rkt")
+
+
+(define num-executed 0)
+
+(define (types? e)
+  (judgment-holds (typed-program ,e TypeEnv)))
+
+(define (has-many-run-statements? prog)
+  (>
+   (count
+    (lambda (cmd)
+       (equal? cmd `(run)))
+     prog)
+   3))
+
+(define (execute prog)
+ (cond
+    [(not (types? prog))
+     (error 'execute "Program does not type check")]
+    [else
+     (define res
+       (apply-reduction-relation* Egglog-Reduction (term (,prog ((tset) (congr) () ())))))
+     (match res
+       [`((() ,database))
+        database]
+       [else (error 'execute (format "Program did not terminate. Got ~a" res))])]))
+
+(define (executes? prog)
+  (cond
+    [(not (types? prog))
+     #t]
+    [(has-many-run-statements? prog)
+     #t]
+    [else
+     (define res
+       (apply-reduction-relation* Egglog-Reduction (term (,prog ((tset) (congr) () ())))))
+     (match res
+       [`((() ,database))
+        (set! num-executed (+ 1 num-executed))
+        #t]
+       [_ #f])]))
+
+(define (check-equal-databases? db1 db2)
+ (match (list db1 db2)
+  [`(((tset ,terms1 ...) (congr ,congr1 ...) ,env1 ,rules1)
+     ((tset ,terms2 ...) (congr ,congr2 ...) ,env2 ,rules2))
+    (and
+      (check-equal? (list->set terms1) (list->set terms2))
+      (check-equal? (list->set congr1) (list->set congr2))
+      (check-equal? env1 env2)
+      (check-equal? rules1 rules2))]
+  [_ (check-equal? db1 db2)]))
+
+(module+ test
+  (check-false
+   (judgment-holds (typed-expr v1 ())))
+  (check-false
+   (judgment-holds
+    (typed-program (v1) TypeEnv)))
+  (check-not-false
+   (judgment-holds
+    (typed-program ((let v1 2) v1)
+           TypeEnv)))
+
+  (check-not-false
+   (judgment-holds
+    (typed-action
+      (cadd v1 v1)
+      ((v1 : no-type))
+      ((v1 : no-type)))))
+  (check-not-false
+   (judgment-holds
+    (typed-actions ((cadd v1 v1)) ((v1 : no-type)) ((v1 : no-type)))))
+  (check-not-false
+   (judgment-holds
+    (typed-query ((= v1 2)) () ((v1 : no-type)))))
+  (check-not-false
+    (judgment-holds
+      (typed-rule
+       (rule ((= v1 2)) ((cadd v1 v1)))
+       ())))
+
+  (check-false
+    (judgment-holds
+      (typed-rule
+       (rule ((= v1 2)) ((cadd v1 v2)))
+       ())))
+  (check-not-false
+   (judgment-holds
+    (typed-query-expr
+      v1
+      ((v2 : no-type))
+      ((v1 : no-type) (v2 : no-type)))))
+  (check-not-false
+   (judgment-holds
+    (typed-query ((= v1 2))
+                 ((v2 : no-type))
+                 TypeEnv)))
+  (check-not-false
+    (judgment-holds
+      (typed-rule
+       (rule ((= v1 2)) ((cadd v1 v2)))
+       ((v2 : no-type)))))
+
+      
+
+  (check-not-false
+   (redex-match Egglog
+                Program
+                (term
+                 ((let v1 2) v1))))
+
+  (check-not-false
+   (redex-match
+    Egglog+Database
+    Database (term ((tset 1 2) (congr (= 1 2)) () ()))))
+
+
+  (check-not-false
+   (redex-match
+    Egglog+Database
+    (Program Database)
+    (term
+     ((skip) ((tset) (congr) () ())))))
+
+  (check-not-false
+   (redex-match
+    Egglog+Database
+    Command+Database
+    (term
+     ((cadd 2 3) ((tset) (congr) () ())))))
+
+
+  (check-equal?
+   (apply-reduction-relation*
+    Command-Reduction
+    (term
+     ((cadd 2 3) ((tset) (congr) () ()))))
+   (list (term (skip ((tset (cadd 2 3)) (congr) () ())))))
+
+  (check-equal?
+   (term (Eval-Expr 2 ()))
+   (term 2))
+  (check-equal?
+   (term (Eval-Expr (cadd 2 3) ()))
+   (term (cadd 2 3)))
+
+  (check-equal-databases?
+   (term
+    (restore-congruence
+      ((tset)
+        (congr (= 1 2)
+        (= 2 3))
+        () ())))
+   '((tset) (congr (= 3 1)
+         (= 2 2)
+         (= 2 1)
+         (= 3 3)
+         (= 3 2)
+         (= 1 3)
+         (= 1 1)
+         (= 1 2)
+         (= 2 3)) () ()))
+
+  (check-equal?
+   (term (restore-congruence
+    ((tset 1) (congr) () ())))
+   (term ((tset 1) (congr (= 1 1)) () ())))
+  
+  (check-true
+    (judgment-holds
+      (tset-is-subset (tset 1) (tset 1)))) 
+  (check-equal?
+   (judgment-holds
+     (valid-env (v1)
+                ((tset 1) (congr (= 1 1)) () ())
+                Env)
+     Env)
+   `(((v1 -> 1))))
+
+  (check-equal?
+    (term (free-vars v1 ()))
+    (term (v1)))
+
+  (check-equal?
+    (judgment-holds (tset-element 1 (tset 1)))
+    #t)
+  
+  (check-equal?
+    (term (Eval-Expr v1 ((v1 -> 1))))
+    (term 1))
+
+  (check-equal?
+    (judgment-holds
+      (valid-env (free-vars v1 ()) ((tset 1) (congr (= 1 1)) () ()) Env)
+      Env)
+    '(((v1 -> 1))))
+
+  (check-equal?
+    (judgment-holds
+      (valid-subst
+        ((tset 1) (congr (= 1 1)) () ()) v1 Env)
+      Env)
+    '(((v1 -> 1))))
+
+  (check-equal?
+   (term
+    (Eval-Local-Actions ()
+      ((tset +inf.0)
+      (congr (= +inf.0 +inf.0))
+      ((v1 -> +inf.0))
+      ((rule () ())))
+      ()))
+   (term
+     ((tset +inf.0)
+      (congr (= +inf.0 +inf.0))
+      ((v1 -> +inf.0))
+      ((rule () ())))))
+
+  (check-equal-databases?
+    (execute
+     (term ((Add 1 2)
+            (rule ((Add a b))
+                  ((Add b a)))
+            (run))))
+    '((tset (Add 1 2) 1 2 (Add 2 1))
+      (congr (= (Add 2 1) (Add 2 1)) (= 2 2) (= 1 1) (= (Add 1 2) (Add 1 2)))
+      ()
+      ((rule ((Add a b)) ((Add b a))))))
+
+  (check-equal-databases?
+   (execute
+    (term ((rule ()
+                 ((let S 16)
+                  (let w (M))
+                  (num w)))
+           (run))))
+    '((tset 16 (M) (num (M)))
+      (congr (= (num (M)) (num (M))) (= (M) (M)) (= 16 16))
+      ()
+      ((rule () ((let S 16) (let w (M)) (num w))))))
+
+  (check-equal-databases?
+   (execute
+    (term ((let v (b 1)) (union 7 7) (union v 4))))
+   (term
+    ((tset (b 1) 4 7 1)
+  (congr (= 4 4) (= 4 (b 1)) (= (b 1) 4) (= 7 7) (= (b 1) (b 1)) (= 1 1))
+  ((v -> (b 1)))
+  ())))
+
+  (check-equal-databases?
+    (execute
+     (term ((union (r) 22)
+            (rule ((r 1) 0 (= (D (q)) 6)) ())
+            (run))))
+    (term ((tset (r) 22)
+        (congr (= (r) (r)) (= 22 22) (= 22 (r)) (= (r) 22))
+        ()
+        ((rule ((r 1) 0 (= (D (q)) 6)) ())))))
+
+  
+  (check-equal-databases?
+   (term
+    (restore-congruence 
+     ((tset 1 2 3)
+      (congr (= 1 2) (= 2 3))
+      () ())))
+   (term ((tset 1 2 3)
+          (congr
+          (= 1 1)
+          (= 3 1)
+          (= 2 2)
+          (= 2 1)
+          (= 3 3)
+          (= 3 2)
+          (= 1 3)
+          (= 1 2)
+          (= 2 3))
+          ()
+          ())))
+
+  (check-equal-databases?
+   (term
+    (restore-congruence
+     ((tset 1 2 (wrapper 2) (wrapper 1))
+      (congr (= 1 2)) () ())))
+   (term ((tset 1 2 (wrapper 2) (wrapper 1))
+          (congr
+            (= (wrapper 2) (wrapper 2))
+            (= 1 1)
+            (= (wrapper 1) (wrapper 1))
+            (= (wrapper 1) (wrapper 2))
+            (= 2 2)
+            (= (wrapper 2) (wrapper 1))
+            (= 2 1)
+            (= 1 2))
+          ()
+          ())))
+
+  (check-equal-databases?
+   (judgment-holds
+     (valid-subst ((tset 1 2 (wrapper 2))
+                   (congr (= 1 2) (= 2 1) (= 1 1) (= 2 2) (= (wrapper 2) (wrapper 2)))
+                   () ())
+                  (wrapper 1)
+                  Env)
+    Env)
+   '(()))
+
+  (check-equal-databases?
+    (execute
+     (term
+       ((Wrapper (Add 1 2))
+        (rule ((Add a b)) ((union (Add a b) (Add b a))))
+        (rule ((= (Wrapper (Add 1 2))
+                  (Wrapper (Add 2 1))))
+              ((success)))
+        (run)
+        (run))))
+    (term ((tset 2 1 (Add 1 2) (Wrapper (Add 1 2)) (Add 2 1) (success))
+  (congr
+   (= (success) (success))
+   (= (Add 2 1) (Add 2 1))
+   (= (Add 2 1) (Add 1 2))
+   (= (Wrapper (Add 1 2)) (Wrapper (Add 1 2)))
+   (= (Add 1 2) (Add 1 2))
+   (= 1 1)
+   (= 2 2)
+   (= (Add 1 2) (Add 2 1)))
+  ()
+  ((rule ((= (Wrapper (Add 1 2)) (Wrapper (Add 2 1)))) ((success)))
+   (rule ((Add a b)) ((union (Add a b) (Add b a))))))))
+
+
+
+  (redex-check Egglog
+               Program
+               (executes? (term Program))
+               #:attempts 200000)
+
+  (displayln (format "Executed ~a programs" num-executed)))
\ No newline at end of file