helm/EXPORT/exportprove/prove/provaF.v

   1 Definition int := (A:Prop)(A->A)->A->A.
   2
   3 Definition O := [A:Prop][s:A->A][o:A]o.
   4
   5 Definition S := [n:int][A:Prop][s:A->A][o:A](s (n A s o)).
   6
   7 Definition Uno := [A:Prop][s:A->A][o:A](s o).
   8
   9 Definition Due := [A:Prop][s:A->A][o:A](s (s o)).
  10
  11 Definition Tre := [A:Prop][s:A->A][o:A](s (s (s o))).
  12
  13 Definition id := [A:Prop][x:A]x.
  14
  15 Definition id_Due := (id int Due).
  16
  17 Definition difficult := ((S Due) (int -> int) (id (int -> int)) (id int)).
  18
  19 Definition is_Zero := [n:int](n int [_:int]Uno O).
  20
  21 Definition couple := [A:Prop][x:A][y:A][z:A->A->A](z x y).
  22
  23 Definition Couple := [A:Prop](z:A->A->A)A.
  24
  25 Definition fst := [A:Prop][x:A][y:A]x.
  26
  27 Definition snd := [A:Prop][x:A][y:A]y.
  28
  29 Definition next : (Couple int) -> (Couple int) := [x:(Couple int)](couple int (x (snd int)) (S (x (snd int)))).
  30
  31 Definition pred := [n:int]((n (Couple int) next (couple int O O))(fst int)).
  32
  33 Definition test := (((pred Tre) (int -> int))(id (int->int)) (id int)).