Stuff moved from old Matita.

[helm.git] / matita / matita / tests / reduction_new.ma

diff --git a/matita/matita/tests/reduction_new.ma b/matita/matita/tests/reduction_new.ma
new file mode 100755 (executable)
index 0000000..b47a750
--- /dev/null
+++ b/matita/matita/tests/reduction_new.ma
@@ -0,0 +1,11 @@
+include "reduction_new_preamble.ma".
+
+ndefinition test:
+ 〈〈x0,x0〉:〈x0,xF〉〉 =
+    ((succ_w16(succ_w16(succ_w16
+    (succ_w16(succ_w16(succ_w16(succ_w16
+    (succ_w16(succ_w16(succ_w16(succ_w16
+    (succ_w16(succ_w16(succ_w16(succ_w16
+     〈〈x0,x0〉:〈x0,x0〉〉)))))))))))))))).
+napply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉); 
+nqed.