FSharp/order.fsx at main · Eggy115/FSharp · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
// ========================================================================= //
// Copyright (c) 2003-2007, John Harrison.                                   //
// Copyright (c) 2012 Eric Taucher, Jack Pappas, Anh-Dung Phan               //
// (See "LICENSE.txt" for details.)                                          //
// ========================================================================= //

#load "initialization.fsx"

open FSharpx.Books.AutomatedReasoning.lib
open FSharpx.Books.AutomatedReasoning.fol
open FSharpx.Books.AutomatedReasoning.order

fsi.AddPrinter sprint_term

// ------------------------------------------------------------------------- //
// This fails the rewrite properties.                                        //
// ------------------------------------------------------------------------- //

let s = parset @"f(x,x,x)";;

let t = parset @"g(x,y)";;

// order.p001
termsize s > termsize t;;

let i = "y" |=> parset @"f(x,x,x)";;

// order.p002
termsize (tsubst i s) > termsize (tsubst i t);;