diff --git a/tranlation-validation/simple/c.k b/tranlation-validation/simple/c.k
new file mode 100644
index 0000000..d56f524
--- /dev/null
+++ b/tranlation-validation/simple/c.k
@@ -0,0 +1,10 @@
+module C
+
+    //=========
+    syntax Bool ::= vars(List)
+    //========
+
+
+
+
+endmodule
\ No newline at end of file
diff --git a/tranlation-validation/simple/empty b/tranlation-validation/simple/empty
new file mode 100644
index 0000000..2c3f05b
--- /dev/null
+++ b/tranlation-validation/simple/empty
@@ -0,0 +1 @@
+@val(12,12,false)
\ No newline at end of file
diff --git a/tranlation-validation/simple/test-spec.k b/tranlation-validation/simple/test-spec.k
new file mode 100644
index 0000000..45716ba
--- /dev/null
+++ b/tranlation-validation/simple/test-spec.k
@@ -0,0 +1,10 @@
+
+module SPEC
+  imports TEST
+
+  rule <k> V:Val => I:Int </k>
+  //requires #noUndef(V)
+
+  //rule <k> V:NUVal => I:Int </k>
+
+endmodule
diff --git a/tranlation-validation/simple/test.k b/tranlation-validation/simple/test.k
new file mode 100644
index 0000000..b0f71b6
--- /dev/null
+++ b/tranlation-validation/simple/test.k
@@ -0,0 +1,30 @@
+//require "c.k"
+
+module TEST
+    //imports C
+
+    syntax Val ::= "@undef" [smtlib(val_undef)]
+    syntax Val ::= "@val" "("Int","Int","Bool")" [smtlib(smt_val)] //int,width,signed
+
+    //syntax Val ::= NUVal
+    //syntax NUVal ::=  "@val" "("Int","Int","Bool")"
+
+
+    //=========
+    //syntax Bool ::= vars(List)
+    //========
+
+
+    configuration
+    <T>
+        <k> $PGM:Val </k>
+    </T>
+
+
+    rule <k> @val(I:Int,_,_) => I </k>
+
+
+    syntax Bool ::= "#noUndef" "(" Val ")" [function]//[function, smtlib(no_undef)]
+    rule #noUndef(@val(_,_,_)) => true //[smt-lemma]
+    rule #noUndef(@undef) => false     //[smt-lemma]
+endmodule
\ No newline at end of file
diff --git a/tranlation-validation/simple/test2-spec.k b/tranlation-validation/simple/test2-spec.k
new file mode 100644
index 0000000..a7349c7
--- /dev/null
+++ b/tranlation-validation/simple/test2-spec.k
@@ -0,0 +1,15 @@
+
+module SPEC
+  imports TEST
+
+
+  rule <k> V:Val </k>
+  //requires #noUndef(V)
+  ensures vars(ListItem(V) ListItem(0))
+
+
+  rule <k> I:Int </k>
+  ensures vars(ListItem(I) ListItem(0))
+  [trusted]
+
+endmodule