mutated_ocaml / testsuite / tests / misc / boyer.ml

Diff from to

testsuite/tests/misc/boyer.ml

 (*                                                                     *)
 (***********************************************************************)
 
-(* $Id: boyer.ml 11156 2011-07-27 14:17:02Z doligez $ *)
+(* $Id: boyer.ml 12800 2012-07-30 18:59:07Z doligez $ *)
 
 (* Manipulations over terms *)
 
       print_string head.name;
       List.iter (fun t -> print_string " "; print_term t) argl;
       print_string ")"
- 
+
 let lemmas = ref ([] : head list)
 
 (* Replacement for property lists *)
 let _ =
 add (CProp
 ("equal",
- [CProp ("compile",[CVar 5]); 
+ [CProp ("compile",[CVar 5]);
   CProp
   ("reverse",
    [CProp ("codegen",[CProp ("optimize",[CVar 5]); CProp ("nil",[])])])]));
 add (CProp
 ("equal",
- [CProp ("eqp",[CVar 23; CVar 24]); 
+ [CProp ("eqp",[CVar 23; CVar 24]);
   CProp ("equal",[CProp ("fix",[CVar 23]); CProp ("fix",[CVar 24])])]));
 add (CProp
 ("equal",
  [CProp ("ge",[CVar 23; CVar 24]); CProp ("le",[CVar 24; CVar 23])]));
 add (CProp
 ("equal",
- [CProp ("boolean",[CVar 23]); 
+ [CProp ("boolean",[CVar 23]);
   CProp
   ("or",
-   [CProp ("equal",[CVar 23; CProp ("true",[])]); 
+   [CProp ("equal",[CVar 23; CProp ("true",[])]);
     CProp ("equal",[CVar 23; CProp ("false",[])])])]));
 add (CProp
 ("equal",
- [CProp ("iff",[CVar 23; CVar 24]); 
+ [CProp ("iff",[CVar 23; CVar 24]);
   CProp
   ("and",
-   [CProp ("implies",[CVar 23; CVar 24]); 
+   [CProp ("implies",[CVar 23; CVar 24]);
     CProp ("implies",[CVar 24; CVar 23])])]));
 add (CProp
 ("equal",
- [CProp ("even1",[CVar 23]); 
+ [CProp ("even1",[CVar 23]);
   CProp
   ("if",
-   [CProp ("zerop",[CVar 23]); CProp ("true",[]); 
+   [CProp ("zerop",[CVar 23]); CProp ("true",[]);
     CProp ("odd",[CProp ("sub1",[CVar 23])])])]));
 add (CProp
 ("equal",
- [CProp ("countps_",[CVar 11; CVar 15]); 
+ [CProp ("countps_",[CVar 11; CVar 15]);
   CProp ("countps_loop",[CVar 11; CVar 15; CProp ("zero",[])])]));
 add (CProp
 ("equal",
- [CProp ("fact_",[CVar 8]); 
+ [CProp ("fact_",[CVar 8]);
   CProp ("fact_loop",[CVar 8; CProp ("one",[])])]));
 add (CProp
 ("equal",
- [CProp ("reverse_",[CVar 23]); 
+ [CProp ("reverse_",[CVar 23]);
   CProp ("reverse_loop",[CVar 23; CProp ("nil",[])])]));
 add (CProp
 ("equal",
- [CProp ("divides",[CVar 23; CVar 24]); 
+ [CProp ("divides",[CVar 23; CVar 24]);
   CProp ("zerop",[CProp ("remainder",[CVar 24; CVar 23])])]));
 add (CProp
 ("equal",
- [CProp ("assume_true",[CVar 21; CVar 0]); 
+ [CProp ("assume_true",[CVar 21; CVar 0]);
   CProp ("cons",[CProp ("cons",[CVar 21; CProp ("true",[])]); CVar 0])]));
 add (CProp
 ("equal",
- [CProp ("assume_false",[CVar 21; CVar 0]); 
+ [CProp ("assume_false",[CVar 21; CVar 0]);
   CProp ("cons",[CProp ("cons",[CVar 21; CProp ("false",[])]); CVar 0])]));
 add (CProp
 ("equal",
- [CProp ("tautology_checker",[CVar 23]); 
+ [CProp ("tautology_checker",[CVar 23]);
   CProp ("tautologyp",[CProp ("normalize",[CVar 23]); CProp ("nil",[])])]));
 add (CProp
 ("equal",
- [CProp ("falsify",[CVar 23]); 
+ [CProp ("falsify",[CVar 23]);
   CProp ("falsify1",[CProp ("normalize",[CVar 23]); CProp ("nil",[])])]));
 add (CProp
 ("equal",
- [CProp ("prime",[CVar 23]); 
+ [CProp ("prime",[CVar 23]);
   CProp
   ("and",
-   [CProp ("not",[CProp ("zerop",[CVar 23])]); 
+   [CProp ("not",[CProp ("zerop",[CVar 23])]);
     CProp
     ("not",
-     [CProp ("equal",[CVar 23; CProp ("add1",[CProp ("zero",[])])])]); 
+     [CProp ("equal",[CVar 23; CProp ("add1",[CProp ("zero",[])])])]);
     CProp ("prime1",[CVar 23; CProp ("sub1",[CVar 23])])])]));
 add (CProp
 ("equal",
- [CProp ("and",[CVar 15; CVar 16]); 
+ [CProp ("and",[CVar 15; CVar 16]);
   CProp
   ("if",
-   [CVar 15; 
-    CProp ("if",[CVar 16; CProp ("true",[]); CProp ("false",[])]); 
+   [CVar 15;
+    CProp ("if",[CVar 16; CProp ("true",[]); CProp ("false",[])]);
     CProp ("false",[])])]));
 add (CProp
 ("equal",
- [CProp ("or",[CVar 15; CVar 16]); 
+ [CProp ("or",[CVar 15; CVar 16]);
   CProp
   ("if",
-   [CVar 15; CProp ("true",[]); 
-    CProp ("if",[CVar 16; CProp ("true",[]); CProp ("false",[])]); 
+   [CVar 15; CProp ("true",[]);
+    CProp ("if",[CVar 16; CProp ("true",[]); CProp ("false",[])]);
     CProp ("false",[])])]));
 add (CProp
 ("equal",
- [CProp ("not",[CVar 15]); 
+ [CProp ("not",[CVar 15]);
   CProp ("if",[CVar 15; CProp ("false",[]); CProp ("true",[])])]));
 add (CProp
 ("equal",
- [CProp ("implies",[CVar 15; CVar 16]); 
+ [CProp ("implies",[CVar 15; CVar 16]);
   CProp
   ("if",
-   [CVar 15; 
-    CProp ("if",[CVar 16; CProp ("true",[]); CProp ("false",[])]); 
+   [CVar 15;
+    CProp ("if",[CVar 16; CProp ("true",[]); CProp ("false",[])]);
     CProp ("true",[])])]));
 add (CProp
 ("equal",
- [CProp ("fix",[CVar 23]); 
+ [CProp ("fix",[CVar 23]);
   CProp ("if",[CProp ("numberp",[CVar 23]); CVar 23; CProp ("zero",[])])]));
 add (CProp
 ("equal",
- [CProp ("if",[CProp ("if",[CVar 0; CVar 1; CVar 2]); CVar 3; CVar 4]); 
+ [CProp ("if",[CProp ("if",[CVar 0; CVar 1; CVar 2]); CVar 3; CVar 4]);
   CProp
   ("if",
-   [CVar 0; CProp ("if",[CVar 1; CVar 3; CVar 4]); 
+   [CVar 0; CProp ("if",[CVar 1; CVar 3; CVar 4]);
     CProp ("if",[CVar 2; CVar 3; CVar 4])])]));
 add (CProp
 ("equal",
- [CProp ("zerop",[CVar 23]); 
+ [CProp ("zerop",[CVar 23]);
   CProp
   ("or",
-   [CProp ("equal",[CVar 23; CProp ("zero",[])]); 
+   [CProp ("equal",[CVar 23; CProp ("zero",[])]);
     CProp ("not",[CProp ("numberp",[CVar 23])])])]));
 add (CProp
 ("equal",
- [CProp ("plus",[CProp ("plus",[CVar 23; CVar 24]); CVar 25]); 
+ [CProp ("plus",[CProp ("plus",[CVar 23; CVar 24]); CVar 25]);
   CProp ("plus",[CVar 23; CProp ("plus",[CVar 24; CVar 25])])]));
 add (CProp
 ("equal",
- [CProp ("equal",[CProp ("plus",[CVar 0; CVar 1]); CProp ("zero",[])]); 
+ [CProp ("equal",[CProp ("plus",[CVar 0; CVar 1]); CProp ("zero",[])]);
   CProp ("and",[CProp ("zerop",[CVar 0]); CProp ("zerop",[CVar 1])])]));
 add (CProp
 ("equal",[CProp ("difference",[CVar 23; CVar 23]); CProp ("zero",[])]));
 ("equal",
  [CProp
   ("equal",
-   [CProp ("plus",[CVar 0; CVar 1]); CProp ("plus",[CVar 0; CVar 2])]); 
+   [CProp ("plus",[CVar 0; CVar 1]); CProp ("plus",[CVar 0; CVar 2])]);
   CProp ("equal",[CProp ("fix",[CVar 1]); CProp ("fix",[CVar 2])])]));
 add (CProp
 ("equal",
  [CProp
-  ("equal",[CProp ("zero",[]); CProp ("difference",[CVar 23; CVar 24])]); 
+  ("equal",[CProp ("zero",[]); CProp ("difference",[CVar 23; CVar 24])]);
   CProp ("not",[CProp ("gt",[CVar 24; CVar 23])])]));
 add (CProp
 ("equal",
- [CProp ("equal",[CVar 23; CProp ("difference",[CVar 23; CVar 24])]); 
+ [CProp ("equal",[CVar 23; CProp ("difference",[CVar 23; CVar 24])]);
   CProp
   ("and",
-   [CProp ("numberp",[CVar 23]); 
+   [CProp ("numberp",[CVar 23]);
     CProp
     ("or",
-     [CProp ("equal",[CVar 23; CProp ("zero",[])]); 
+     [CProp ("equal",[CVar 23; CProp ("zero",[])]);
       CProp ("zerop",[CVar 24])])])]));
 add (CProp
 ("equal",
  [CProp
   ("meaning",
-   [CProp ("plus_tree",[CProp ("append",[CVar 23; CVar 24])]); CVar 0]); 
+   [CProp ("plus_tree",[CProp ("append",[CVar 23; CVar 24])]); CVar 0]);
   CProp
   ("plus",
-   [CProp ("meaning",[CProp ("plus_tree",[CVar 23]); CVar 0]); 
+   [CProp ("meaning",[CProp ("plus_tree",[CVar 23]); CVar 0]);
     CProp ("meaning",[CProp ("plus_tree",[CVar 24]); CVar 0])])]));
 add (CProp
 ("equal",
  [CProp
   ("meaning",
-   [CProp ("plus_tree",[CProp ("plus_fringe",[CVar 23])]); CVar 0]); 
+   [CProp ("plus_tree",[CProp ("plus_fringe",[CVar 23])]); CVar 0]);
   CProp ("fix",[CProp ("meaning",[CVar 23; CVar 0])])]));
 add (CProp
 ("equal",
- [CProp ("append",[CProp ("append",[CVar 23; CVar 24]); CVar 25]); 
+ [CProp ("append",[CProp ("append",[CVar 23; CVar 24]); CVar 25]);
   CProp ("append",[CVar 23; CProp ("append",[CVar 24; CVar 25])])]));
 add (CProp
 ("equal",
- [CProp ("reverse",[CProp ("append",[CVar 0; CVar 1])]); 
+ [CProp ("reverse",[CProp ("append",[CVar 0; CVar 1])]);
   CProp
   ("append",[CProp ("reverse",[CVar 1]); CProp ("reverse",[CVar 0])])]));
 add (CProp
 ("equal",
- [CProp ("times",[CVar 23; CProp ("plus",[CVar 24; CVar 25])]); 
+ [CProp ("times",[CVar 23; CProp ("plus",[CVar 24; CVar 25])]);
   CProp
   ("plus",
-   [CProp ("times",[CVar 23; CVar 24]); 
+   [CProp ("times",[CVar 23; CVar 24]);
     CProp ("times",[CVar 23; CVar 25])])]));
 add (CProp
 ("equal",
- [CProp ("times",[CProp ("times",[CVar 23; CVar 24]); CVar 25]); 
+ [CProp ("times",[CProp ("times",[CVar 23; CVar 24]); CVar 25]);
   CProp ("times",[CVar 23; CProp ("times",[CVar 24; CVar 25])])]));
 add (CProp
 ("equal",
  [CProp
-  ("equal",[CProp ("times",[CVar 23; CVar 24]); CProp ("zero",[])]); 
+  ("equal",[CProp ("times",[CVar 23; CVar 24]); CProp ("zero",[])]);
   CProp ("or",[CProp ("zerop",[CVar 23]); CProp ("zerop",[CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("exec",[CProp ("append",[CVar 23; CVar 24]); CVar 15; CVar 4]); 
+ [CProp ("exec",[CProp ("append",[CVar 23; CVar 24]); CVar 15; CVar 4]);
   CProp
   ("exec",[CVar 24; CProp ("exec",[CVar 23; CVar 15; CVar 4]); CVar 4])]));
 add (CProp
 ("equal",
- [CProp ("mc_flatten",[CVar 23; CVar 24]); 
+ [CProp ("mc_flatten",[CVar 23; CVar 24]);
   CProp ("append",[CProp ("flatten",[CVar 23]); CVar 24])]));
 add (CProp
 ("equal",
- [CProp ("member",[CVar 23; CProp ("append",[CVar 0; CVar 1])]); 
+ [CProp ("member",[CVar 23; CProp ("append",[CVar 0; CVar 1])]);
   CProp
   ("or",
-   [CProp ("member",[CVar 23; CVar 0]); 
+   [CProp ("member",[CVar 23; CVar 0]);
     CProp ("member",[CVar 23; CVar 1])])]));
 add (CProp
 ("equal",
- [CProp ("member",[CVar 23; CProp ("reverse",[CVar 24])]); 
+ [CProp ("member",[CVar 23; CProp ("reverse",[CVar 24])]);
   CProp ("member",[CVar 23; CVar 24])]));
 add (CProp
 ("equal",
- [CProp ("length",[CProp ("reverse",[CVar 23])]); 
+ [CProp ("length",[CProp ("reverse",[CVar 23])]);
   CProp ("length",[CVar 23])]));
 add (CProp
 ("equal",
- [CProp ("member",[CVar 0; CProp ("intersect",[CVar 1; CVar 2])]); 
+ [CProp ("member",[CVar 0; CProp ("intersect",[CVar 1; CVar 2])]);
   CProp
   ("and",
    [CProp ("member",[CVar 0; CVar 1]); CProp ("member",[CVar 0; CVar 2])])]));
 ("equal",[CProp ("nth",[CProp ("zero",[]); CVar 8]); CProp ("zero",[])]));
 add (CProp
 ("equal",
- [CProp ("exp",[CVar 8; CProp ("plus",[CVar 9; CVar 10])]); 
+ [CProp ("exp",[CVar 8; CProp ("plus",[CVar 9; CVar 10])]);
   CProp
   ("times",
    [CProp ("exp",[CVar 8; CVar 9]); CProp ("exp",[CVar 8; CVar 10])])]));
 add (CProp
 ("equal",
- [CProp ("exp",[CVar 8; CProp ("times",[CVar 9; CVar 10])]); 
+ [CProp ("exp",[CVar 8; CProp ("times",[CVar 9; CVar 10])]);
   CProp ("exp",[CProp ("exp",[CVar 8; CVar 9]); CVar 10])]));
 add (CProp
 ("equal",
- [CProp ("reverse_loop",[CVar 23; CVar 24]); 
+ [CProp ("reverse_loop",[CVar 23; CVar 24]);
   CProp ("append",[CProp ("reverse",[CVar 23]); CVar 24])]));
 add (CProp
 ("equal",
- [CProp ("reverse_loop",[CVar 23; CProp ("nil",[])]); 
+ [CProp ("reverse_loop",[CVar 23; CProp ("nil",[])]);
   CProp ("reverse",[CVar 23])]));
 add (CProp
 ("equal",
- [CProp ("count_list",[CVar 25; CProp ("sort_lp",[CVar 23; CVar 24])]); 
+ [CProp ("count_list",[CVar 25; CProp ("sort_lp",[CVar 23; CVar 24])]);
   CProp
   ("plus",
-   [CProp ("count_list",[CVar 25; CVar 23]); 
+   [CProp ("count_list",[CVar 25; CVar 23]);
     CProp ("count_list",[CVar 25; CVar 24])])]));
 add (CProp
 ("equal",
  [CProp
   ("equal",
-   [CProp ("append",[CVar 0; CVar 1]); CProp ("append",[CVar 0; CVar 2])]); 
+   [CProp ("append",[CVar 0; CVar 1]); CProp ("append",[CVar 0; CVar 2])]);
   CProp ("equal",[CVar 1; CVar 2])]));
 add (CProp
 ("equal",
  [CProp
   ("plus",
-   [CProp ("remainder",[CVar 23; CVar 24]); 
-    CProp ("times",[CVar 24; CProp ("quotient",[CVar 23; CVar 24])])]); 
+   [CProp ("remainder",[CVar 23; CVar 24]);
+    CProp ("times",[CVar 24; CProp ("quotient",[CVar 23; CVar 24])])]);
   CProp ("fix",[CVar 23])]));
 add (CProp
 ("equal",
  [CProp
-  ("power_eval",[CProp ("big_plus",[CVar 11; CVar 8; CVar 1]); CVar 1]); 
+  ("power_eval",[CProp ("big_plus",[CVar 11; CVar 8; CVar 1]); CVar 1]);
   CProp ("plus",[CProp ("power_eval",[CVar 11; CVar 1]); CVar 8])]));
 add (CProp
 ("equal",
  [CProp
   ("power_eval",
-   [CProp ("big_plus",[CVar 23; CVar 24; CVar 8; CVar 1]); CVar 1]); 
+   [CProp ("big_plus",[CVar 23; CVar 24; CVar 8; CVar 1]); CVar 1]);
   CProp
   ("plus",
-   [CVar 8; 
+   [CVar 8;
     CProp
     ("plus",
-     [CProp ("power_eval",[CVar 23; CVar 1]); 
+     [CProp ("power_eval",[CVar 23; CVar 1]);
       CProp ("power_eval",[CVar 24; CVar 1])])])]));
 add (CProp
 ("equal",
  [CProp ("remainder",[CVar 24; CProp ("one",[])]); CProp ("zero",[])]));
 add (CProp
 ("equal",
- [CProp ("lt",[CProp ("remainder",[CVar 23; CVar 24]); CVar 24]); 
+ [CProp ("lt",[CProp ("remainder",[CVar 23; CVar 24]); CVar 24]);
   CProp ("not",[CProp ("zerop",[CVar 24])])]));
 add (CProp
 ("equal",[CProp ("remainder",[CVar 23; CVar 23]); CProp ("zero",[])]));
 add (CProp
 ("equal",
- [CProp ("lt",[CProp ("quotient",[CVar 8; CVar 9]); CVar 8]); 
+ [CProp ("lt",[CProp ("quotient",[CVar 8; CVar 9]); CVar 8]);
   CProp
   ("and",
-   [CProp ("not",[CProp ("zerop",[CVar 8])]); 
+   [CProp ("not",[CProp ("zerop",[CVar 8])]);
     CProp
     ("or",
-     [CProp ("zerop",[CVar 9]); 
+     [CProp ("zerop",[CVar 9]);
       CProp ("not",[CProp ("equal",[CVar 9; CProp ("one",[])])])])])]));
 add (CProp
 ("equal",
- [CProp ("lt",[CProp ("remainder",[CVar 23; CVar 24]); CVar 23]); 
+ [CProp ("lt",[CProp ("remainder",[CVar 23; CVar 24]); CVar 23]);
   CProp
   ("and",
-   [CProp ("not",[CProp ("zerop",[CVar 24])]); 
-    CProp ("not",[CProp ("zerop",[CVar 23])]); 
+   [CProp ("not",[CProp ("zerop",[CVar 24])]);
+    CProp ("not",[CProp ("zerop",[CVar 23])]);
     CProp ("not",[CProp ("lt",[CVar 23; CVar 24])])])]));
 add (CProp
 ("equal",
- [CProp ("power_eval",[CProp ("power_rep",[CVar 8; CVar 1]); CVar 1]); 
+ [CProp ("power_eval",[CProp ("power_rep",[CVar 8; CVar 1]); CVar 1]);
   CProp ("fix",[CVar 8])]));
 add (CProp
 ("equal",
   ("power_eval",
    [CProp
     ("big_plus",
-     [CProp ("power_rep",[CVar 8; CVar 1]); 
-      CProp ("power_rep",[CVar 9; CVar 1]); CProp ("zero",[]); 
-      CVar 1]); 
-    CVar 1]); 
+     [CProp ("power_rep",[CVar 8; CVar 1]);
+      CProp ("power_rep",[CVar 9; CVar 1]); CProp ("zero",[]);
+      CVar 1]);
+    CVar 1]);
   CProp ("plus",[CVar 8; CVar 9])]));
 add (CProp
 ("equal",
  [CProp ("gcd",[CVar 23; CVar 24]); CProp ("gcd",[CVar 24; CVar 23])]));
 add (CProp
 ("equal",
- [CProp ("nth",[CProp ("append",[CVar 0; CVar 1]); CVar 8]); 
+ [CProp ("nth",[CProp ("append",[CVar 0; CVar 1]); CVar 8]);
   CProp
   ("append",
-   [CProp ("nth",[CVar 0; CVar 8]); 
+   [CProp ("nth",[CVar 0; CVar 8]);
     CProp
     ("nth",
      [CVar 1; CProp ("difference",[CVar 8; CProp ("length",[CVar 0])])])])]));
 add (CProp
 ("equal",
- [CProp ("difference",[CProp ("plus",[CVar 23; CVar 24]); CVar 23]); 
+ [CProp ("difference",[CProp ("plus",[CVar 23; CVar 24]); CVar 23]);
   CProp ("fix",[CVar 24])]));
 add (CProp
 ("equal",
- [CProp ("difference",[CProp ("plus",[CVar 24; CVar 23]); CVar 23]); 
+ [CProp ("difference",[CProp ("plus",[CVar 24; CVar 23]); CVar 23]);
   CProp ("fix",[CVar 24])]));
 add (CProp
 ("equal",
  [CProp
   ("difference",
-   [CProp ("plus",[CVar 23; CVar 24]); CProp ("plus",[CVar 23; CVar 25])]); 
+   [CProp ("plus",[CVar 23; CVar 24]); CProp ("plus",[CVar 23; CVar 25])]);
   CProp ("difference",[CVar 24; CVar 25])]));
 add (CProp
 ("equal",
- [CProp ("times",[CVar 23; CProp ("difference",[CVar 2; CVar 22])]); 
+ [CProp ("times",[CVar 23; CProp ("difference",[CVar 2; CVar 22])]);
   CProp
   ("difference",
-   [CProp ("times",[CVar 2; CVar 23]); 
+   [CProp ("times",[CVar 2; CVar 23]);
     CProp ("times",[CVar 22; CVar 23])])]));
 add (CProp
 ("equal",
- [CProp ("remainder",[CProp ("times",[CVar 23; CVar 25]); CVar 25]); 
+ [CProp ("remainder",[CProp ("times",[CVar 23; CVar 25]); CVar 25]);
   CProp ("zero",[])]));
 add (CProp
 ("equal",
  [CProp
   ("difference",
-   [CProp ("plus",[CVar 1; CProp ("plus",[CVar 0; CVar 2])]); CVar 0]); 
+   [CProp ("plus",[CVar 1; CProp ("plus",[CVar 0; CVar 2])]); CVar 0]);
   CProp ("plus",[CVar 1; CVar 2])]));
 add (CProp
 ("equal",
  [CProp
   ("difference",
-   [CProp ("add1",[CProp ("plus",[CVar 24; CVar 25])]); CVar 25]); 
+   [CProp ("add1",[CProp ("plus",[CVar 24; CVar 25])]); CVar 25]);
   CProp ("add1",[CVar 24])]));
 add (CProp
 ("equal",
  [CProp
   ("lt",
-   [CProp ("plus",[CVar 23; CVar 24]); CProp ("plus",[CVar 23; CVar 25])]); 
+   [CProp ("plus",[CVar 23; CVar 24]); CProp ("plus",[CVar 23; CVar 25])]);
   CProp ("lt",[CVar 24; CVar 25])]));
 add (CProp
 ("equal",
  [CProp
   ("lt",
-   [CProp ("times",[CVar 23; CVar 25]); 
-    CProp ("times",[CVar 24; CVar 25])]); 
+   [CProp ("times",[CVar 23; CVar 25]);
+    CProp ("times",[CVar 24; CVar 25])]);
   CProp
   ("and",
-   [CProp ("not",[CProp ("zerop",[CVar 25])]); 
+   [CProp ("not",[CProp ("zerop",[CVar 25])]);
     CProp ("lt",[CVar 23; CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("lt",[CVar 24; CProp ("plus",[CVar 23; CVar 24])]); 
+ [CProp ("lt",[CVar 24; CProp ("plus",[CVar 23; CVar 24])]);
   CProp ("not",[CProp ("zerop",[CVar 23])])]));
 add (CProp
 ("equal",
  [CProp
   ("gcd",
-   [CProp ("times",[CVar 23; CVar 25]); 
-    CProp ("times",[CVar 24; CVar 25])]); 
+   [CProp ("times",[CVar 23; CVar 25]);
+    CProp ("times",[CVar 24; CVar 25])]);
   CProp ("times",[CVar 25; CProp ("gcd",[CVar 23; CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("value",[CProp ("normalize",[CVar 23]); CVar 0]); 
+ [CProp ("value",[CProp ("normalize",[CVar 23]); CVar 0]);
   CProp ("value",[CVar 23; CVar 0])]));
 add (CProp
 ("equal",
  [CProp
   ("equal",
-   [CProp ("flatten",[CVar 23]); 
-    CProp ("cons",[CVar 24; CProp ("nil",[])])]); 
+   [CProp ("flatten",[CVar 23]);
+    CProp ("cons",[CVar 24; CProp ("nil",[])])]);
   CProp
   ("and",
    [CProp ("nlistp",[CVar 23]); CProp ("equal",[CVar 23; CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("listp",[CProp ("gother",[CVar 23])]); 
+ [CProp ("listp",[CProp ("gother",[CVar 23])]);
   CProp ("listp",[CVar 23])]));
 add (CProp
 ("equal",
- [CProp ("samefringe",[CVar 23; CVar 24]); 
+ [CProp ("samefringe",[CVar 23; CVar 24]);
   CProp
   ("equal",[CProp ("flatten",[CVar 23]); CProp ("flatten",[CVar 24])])]));
 add (CProp
 ("equal",
  [CProp
   ("equal",
-   [CProp ("greatest_factor",[CVar 23; CVar 24]); CProp ("zero",[])]); 
+   [CProp ("greatest_factor",[CVar 23; CVar 24]); CProp ("zero",[])]);
   CProp
   ("and",
    [CProp
     ("or",
-     [CProp ("zerop",[CVar 24]); 
-      CProp ("equal",[CVar 24; CProp ("one",[])])]); 
+     [CProp ("zerop",[CVar 24]);
+      CProp ("equal",[CVar 24; CProp ("one",[])])]);
     CProp ("equal",[CVar 23; CProp ("zero",[])])])]));
 add (CProp
 ("equal",
  [CProp
   ("equal",
-   [CProp ("greatest_factor",[CVar 23; CVar 24]); CProp ("one",[])]); 
+   [CProp ("greatest_factor",[CVar 23; CVar 24]); CProp ("one",[])]);
   CProp ("equal",[CVar 23; CProp ("one",[])])]));
 add (CProp
 ("equal",
- [CProp ("numberp",[CProp ("greatest_factor",[CVar 23; CVar 24])]); 
+ [CProp ("numberp",[CProp ("greatest_factor",[CVar 23; CVar 24])]);
   CProp
   ("not",
    [CProp
     ("and",
      [CProp
       ("or",
-       [CProp ("zerop",[CVar 24]); 
-        CProp ("equal",[CVar 24; CProp ("one",[])])]); 
+       [CProp ("zerop",[CVar 24]);
+        CProp ("equal",[CVar 24; CProp ("one",[])])]);
       CProp ("not",[CProp ("numberp",[CVar 23])])])])]));
 add (CProp
 ("equal",
- [CProp ("times_list",[CProp ("append",[CVar 23; CVar 24])]); 
+ [CProp ("times_list",[CProp ("append",[CVar 23; CVar 24])]);
   CProp
   ("times",
    [CProp ("times_list",[CVar 23]); CProp ("times_list",[CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("prime_list",[CProp ("append",[CVar 23; CVar 24])]); 
+ [CProp ("prime_list",[CProp ("append",[CVar 23; CVar 24])]);
   CProp
   ("and",
    [CProp ("prime_list",[CVar 23]); CProp ("prime_list",[CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("equal",[CVar 25; CProp ("times",[CVar 22; CVar 25])]); 
+ [CProp ("equal",[CVar 25; CProp ("times",[CVar 22; CVar 25])]);
   CProp
   ("and",
-   [CProp ("numberp",[CVar 25]); 
+   [CProp ("numberp",[CVar 25]);
     CProp
     ("or",
-     [CProp ("equal",[CVar 25; CProp ("zero",[])]); 
+     [CProp ("equal",[CVar 25; CProp ("zero",[])]);
       CProp ("equal",[CVar 22; CProp ("one",[])])])])]));
 add (CProp
 ("equal",
- [CProp ("ge",[CVar 23; CVar 24]); 
+ [CProp ("ge",[CVar 23; CVar 24]);
   CProp ("not",[CProp ("lt",[CVar 23; CVar 24])])]));
 add (CProp
 ("equal",
- [CProp ("equal",[CVar 23; CProp ("times",[CVar 23; CVar 24])]); 
+ [CProp ("equal",[CVar 23; CProp ("times",[CVar 23; CVar 24])]);
   CProp
   ("or",
-   [CProp ("equal",[CVar 23; CProp ("zero",[])]); 
+   [CProp ("equal",[CVar 23; CProp ("zero",[])]);
     CProp
     ("and",
-     [CProp ("numberp",[CVar 23]); 
+     [CProp ("numberp",[CVar 23]);
       CProp ("equal",[CVar 24; CProp ("one",[])])])])]));
 add (CProp
 ("equal",
- [CProp ("remainder",[CProp ("times",[CVar 24; CVar 23]); CVar 24]); 
+ [CProp ("remainder",[CProp ("times",[CVar 24; CVar 23]); CVar 24]);
   CProp ("zero",[])]));
 add (CProp
 ("equal",
- [CProp ("equal",[CProp ("times",[CVar 0; CVar 1]); CProp ("one",[])]); 
+ [CProp ("equal",[CProp ("times",[CVar 0; CVar 1]); CProp ("one",[])]);
   CProp
   ("and",
-   [CProp ("not",[CProp ("equal",[CVar 0; CProp ("zero",[])])]); 
-    CProp ("not",[CProp ("equal",[CVar 1; CProp ("zero",[])])]); 
-    CProp ("numberp",[CVar 0]); CProp ("numberp",[CVar 1]); 
-    CProp ("equal",[CProp ("sub1",[CVar 0]); CProp ("zero",[])]); 
+   [CProp ("not",[CProp ("equal",[CVar 0; CProp ("zero",[])])]);
+    CProp ("not",[CProp ("equal",[CVar 1; CProp ("zero",[])])]);
+    CProp ("numberp",[CVar 0]); CProp ("numberp",[CVar 1]);
+    CProp ("equal",[CProp ("sub1",[CVar 0]); CProp ("zero",[])]);
     CProp ("equal",[CProp ("sub1",[CVar 1]); CProp ("zero",[])])])]));
 add (CProp
 ("equal",
  [CProp
   ("lt",
-   [CProp ("length",[CProp ("delete",[CVar 23; CVar 11])]); 
-    CProp ("length",[CVar 11])]); 
+   [CProp ("length",[CProp ("delete",[CVar 23; CVar 11])]);
+    CProp ("length",[CVar 11])]);
   CProp ("member",[CVar 23; CVar 11])]));
 add (CProp
 ("equal",
- [CProp ("sort2",[CProp ("delete",[CVar 23; CVar 11])]); 
+ [CProp ("sort2",[CProp ("delete",[CVar 23; CVar 11])]);
   CProp ("delete",[CVar 23; CProp ("sort2",[CVar 11])])]));
 add (CProp ("equal",[CProp ("dsort",[CVar 23]); CProp ("sort2",[CVar 23])]));
 add (CProp
   ("length",
    [CProp
     ("cons",
-     [CVar 0; 
+     [CVar 0;
       CProp
       ("cons",
-       [CVar 1; 
+       [CVar 1;
         CProp
         ("cons",
-         [CVar 2; 
+         [CVar 2;
           CProp
           ("cons",
-           [CVar 3; 
+           [CVar 3;
             CProp ("cons",[CVar 4; CProp ("cons",[CVar 5; CVar 6])])])])])])])
   ; CProp ("plus",[CProp ("six",[]); CProp ("length",[CVar 6])])]));
 add (CProp
 ("equal",
  [CProp
   ("difference",
-   [CProp ("add1",[CProp ("add1",[CVar 23])]); CProp ("two",[])]); 
+   [CProp ("add1",[CProp ("add1",[CVar 23])]); CProp ("two",[])]);
   CProp ("fix",[CVar 23])]));
 add (CProp
 ("equal",
  [CProp
   ("quotient",
-   [CProp ("plus",[CVar 23; CProp ("plus",[CVar 23; CVar 24])]); 
-    CProp ("two",[])]); 
+   [CProp ("plus",[CVar 23; CProp ("plus",[CVar 23; CVar 24])]);
+    CProp ("two",[])]);
   CProp
   ("plus",[CVar 23; CProp ("quotient",[CVar 24; CProp ("two",[])])])]));
 add (CProp
 ("equal",
- [CProp ("sigma",[CProp ("zero",[]); CVar 8]); 
+ [CProp ("sigma",[CProp ("zero",[]); CVar 8]);
   CProp
   ("quotient",
    [CProp ("times",[CVar 8; CProp ("add1",[CVar 8])]); CProp ("two",[])])]));
 add (CProp
 ("equal",
- [CProp ("plus",[CVar 23; CProp ("add1",[CVar 24])]); 
+ [CProp ("plus",[CVar 23; CProp ("add1",[CVar 24])]);
   CProp
   ("if",
-   [CProp ("numberp",[CVar 24]); 
-    CProp ("add1",[CProp ("plus",[CVar 23; CVar 24])]); 
+   [CProp ("numberp",[CVar 24]);
+    CProp ("add1",[CProp ("plus",[CVar 23; CVar 24])]);
     CProp ("add1",[CVar 23])])]));
 add (CProp
 ("equal",
  [CProp
   ("equal",
-   [CProp ("difference",[CVar 23; CVar 24]); 
-    CProp ("difference",[CVar 25; CVar 24])]); 
+   [CProp ("difference",[CVar 23; CVar 24]);
+    CProp ("difference",[CVar 25; CVar 24])]);
   CProp
   ("if",
-   [CProp ("lt",[CVar 23; CVar 24]); 
-    CProp ("not",[CProp ("lt",[CVar 24; CVar 25])]); 
+   [CProp ("lt",[CVar 23; CVar 24]);
+    CProp ("not",[CProp ("lt",[CVar 24; CVar 25])]);
     CProp
     ("if",
-     [CProp ("lt",[CVar 25; CVar 24]); 
-      CProp ("not",[CProp ("lt",[CVar 24; CVar 23])]); 
+     [CProp ("lt",[CVar 25; CVar 24]);
+      CProp ("not",[CProp ("lt",[CVar 24; CVar 23])]);
       CProp ("equal",[CProp ("fix",[CVar 23]); CProp ("fix",[CVar 25])])])])])
 );
 add (CProp
 ("equal",
  [CProp
   ("meaning",
-   [CProp ("plus_tree",[CProp ("delete",[CVar 23; CVar 24])]); CVar 0]); 
+   [CProp ("plus_tree",[CProp ("delete",[CVar 23; CVar 24])]); CVar 0]);
   CProp
   ("if",
-   [CProp ("member",[CVar 23; CVar 24]); 
+   [CProp ("member",[CVar 23; CVar 24]);
     CProp
     ("difference",
-     [CProp ("meaning",[CProp ("plus_tree",[CVar 24]); CVar 0]); 
-      CProp ("meaning",[CVar 23; CVar 0])]); 
+     [CProp ("meaning",[CProp ("plus_tree",[CVar 24]); CVar 0]);
+      CProp ("meaning",[CVar 23; CVar 0])]);
     CProp ("meaning",[CProp ("plus_tree",[CVar 24]); CVar 0])])]));
 add (CProp
 ("equal",
- [CProp ("times",[CVar 23; CProp ("add1",[CVar 24])]); 
+ [CProp ("times",[CVar 23; CProp ("add1",[CVar 24])]);
   CProp
   ("if",
-   [CProp ("numberp",[CVar 24]); 
+   [CProp ("numberp",[CVar 24]);
     CProp
     ("plus",
-     [CVar 23; CProp ("times",[CVar 23; CVar 24]); 
+     [CVar 23; CProp ("times",[CVar 23; CVar 24]);
       CProp ("fix",[CVar 23])])])]));
 add (CProp
 ("equal",
- [CProp ("nth",[CProp ("nil",[]); CVar 8]); 
+ [CProp ("nth",[CProp ("nil",[]); CVar 8]);
   CProp
   ("if",[CProp ("zerop",[CVar 8]); CProp ("nil",[]); CProp ("zero",[])])]));
 add (CProp
 ("equal",
- [CProp ("last",[CProp ("append",[CVar 0; CVar 1])]); 
+ [CProp ("last",[CProp ("append",[CVar 0; CVar 1])]);
   CProp
   ("if",
-   [CProp ("listp",[CVar 1]); CProp ("last",[CVar 1]); 
+   [CProp ("listp",[CVar 1]); CProp ("last",[CVar 1]);
     CProp
     ("if",
-     [CProp ("listp",[CVar 0]); 
-      CProp ("cons",[CProp ("car",[CProp ("last",[CVar 0])]); CVar 1]); 
+     [CProp ("listp",[CVar 0]);
+      CProp ("cons",[CProp ("car",[CProp ("last",[CVar 0])]); CVar 1]);
       CVar 1])])]));
 add (CProp
 ("equal",
- [CProp ("equal",[CProp ("lt",[CVar 23; CVar 24]); CVar 25]); 
+ [CProp ("equal",[CProp ("lt",[CVar 23; CVar 24]); CVar 25]);
   CProp
   ("if",
-   [CProp ("lt",[CVar 23; CVar 24]); 
-    CProp ("equal",[CProp ("true",[]); CVar 25]); 
+   [CProp ("lt",[CVar 23; CVar 24]);
+    CProp ("equal",[CProp ("true",[]); CVar 25]);
     CProp ("equal",[CProp ("false",[]); CVar 25])])]));
 add (CProp
 ("equal",
- [CProp ("assignment",[CVar 23; CProp ("append",[CVar 0; CVar 1])]); 
+ [CProp ("assignment",[CVar 23; CProp ("append",[CVar 0; CVar 1])]);
   CProp
   ("if",
-   [CProp ("assignedp",[CVar 23; CVar 0]); 
-    CProp ("assignment",[CVar 23; CVar 0]); 
+   [CProp ("assignedp",[CVar 23; CVar 0]);
+    CProp ("assignment",[CVar 23; CVar 0]);
     CProp ("assignment",[CVar 23; CVar 1])])]));
 add (CProp
 ("equal",
- [CProp ("car",[CProp ("gother",[CVar 23])]); 
+ [CProp ("car",[CProp ("gother",[CVar 23])]);
   CProp
   ("if",
-   [CProp ("listp",[CVar 23]); 
+   [CProp ("listp",[CVar 23]);
     CProp ("car",[CProp ("flatten",[CVar 23])]); CProp ("zero",[])])]));
 add (CProp
 ("equal",
- [CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar 23])])]); 
+ [CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar 23])])]);
   CProp
   ("if",
-   [CProp ("listp",[CVar 23]); 
-    CProp ("cdr",[CProp ("flatten",[CVar 23])]); 
+   [CProp ("listp",[CVar 23]);
+    CProp ("cdr",[CProp ("flatten",[CVar 23])]);
     CProp ("cons",[CProp ("zero",[]); CProp ("nil",[])])])]));
 add (CProp
 ("equal",
- [CProp ("quotient",[CProp ("times",[CVar 24; CVar 23]); CVar 24]); 
+ [CProp ("quotient",[CProp ("times",[CVar 24; CVar 23]); CVar 24]);
   CProp
   ("if",
-   [CProp ("zerop",[CVar 24]); CProp ("zero",[]); 
+   [CProp ("zerop",[CVar 24]); CProp ("zero",[]);
     CProp ("fix",[CVar 23])])]));
 add (CProp
 ("equal",
- [CProp ("get",[CVar 9; CProp ("set",[CVar 8; CVar 21; CVar 12])]); 
+ [CProp ("get",[CVar 9; CProp ("set",[CVar 8; CVar 21; CVar 12])]);
   CProp
   ("if",
-   [CProp ("eqp",[CVar 9; CVar 8]); CVar 21; 
+   [CProp ("eqp",[CVar 9; CVar 8]); CVar 21;
     CProp ("get",[CVar 9; CVar 12])])]))
 
 (* Tautology checker *)
   end
 
 
-let tautp x = 
+let tautp x =
 (*  print_term x; print_string"\n"; *)
   let y = rewrite x in
 (*    print_term y; print_string "\n"; *)
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.