...

[helm.git] / helm / software / matita / tests / reduction_old.ma

diff --git a/helm/software/matita/tests/reduction_old.ma b/helm/software/matita/tests/reduction_old.ma
new file mode 100755 (executable)
index 0000000..b0596ae
--- /dev/null
+++ b/helm/software/matita/tests/reduction_old.ma
@@ -0,0 +1,10 @@
+include "reduction_old_preamble.ma".
+definition 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〉〉)))))))))))))))).
+apply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉); 
+qed.