Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / exportprove / prove / provaF.v

diff --git a/helm/EXPORT/exportprove/prove/provaF.v b/helm/EXPORT/exportprove/prove/provaF.v
new file mode 100644 (file)
index 0000000..072010f
--- /dev/null
+++ b/helm/EXPORT/exportprove/prove/provaF.v
@@ -0,0 +1,33 @@
+Definition int := (A:Prop)(A->A)->A->A.
+
+Definition O := [A:Prop][s:A->A][o:A]o.
+
+Definition S := [n:int][A:Prop][s:A->A][o:A](s (n A s o)).
+
+Definition Uno := [A:Prop][s:A->A][o:A](s o).
+
+Definition Due := [A:Prop][s:A->A][o:A](s (s o)).
+
+Definition Tre := [A:Prop][s:A->A][o:A](s (s (s o))).
+
+Definition id := [A:Prop][x:A]x.
+
+Definition id_Due := (id int Due).
+
+Definition difficult := ((S Due) (int -> int) (id (int -> int)) (id int)).
+
+Definition is_Zero := [n:int](n int [_:int]Uno O).
+
+Definition couple := [A:Prop][x:A][y:A][z:A->A->A](z x y).
+
+Definition Couple := [A:Prop](z:A->A->A)A.
+
+Definition fst := [A:Prop][x:A][y:A]x.
+
+Definition snd := [A:Prop][x:A][y:A]y.
+
+Definition next : (Couple int) -> (Couple int) := [x:(Couple int)](couple int (x (snd int)) (S (x (snd int)))).
+
+Definition pred := [n:int]((n (Couple int) next (couple int O O))(fst int)).
+
+Definition test := (((pred Tre) (int -> int))(id (int->int)) (id int)).