10139N/ACopyright (c) 2002-5 CUTS and contributors.
13666N/ARunning with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
10139N/ALoading theory "HsHOLCF" (required by "ex_class_hc")
10139N/A fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
10139N/A sig val initialize : string list -> unit val record : string -> unit end
10139N/A### "'a Prelude_Color -> 'a Prelude_Color -> tr"
10139N/A### is strictly less general than the declared type
10139N/A### "'a Prelude_Color -> tr -> 'a Prelude_Color Prelude_Color"
10139N/A### is strictly less general than the declared type
10139N/A### "'a Prelude_MyList -> 'a Prelude_MyList -> tr"
10139N/A### is strictly less general than the declared type
10139N/A### "'a Prelude_MyList -> tr -> 'a Prelude_MyList Prelude_Color"
10139N/A### is strictly less general than the declared type
10139N/A### "('a, 'b) Prelude_MPList -> ('a, 'b) Prelude_MPList -> tr"
10139N/A### is strictly less general than the declared type
10139N/A### "('a, 'b) Prelude_MPList -> tr -> ('a, 'b) Prelude_MPList Prelude_Color"
10139N/A### is strictly less general than the declared type
10139N/A {ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
10139N/A Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
10139N/A Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
10139N/A Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
10139N/A Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
10139N/A Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
10139N/A Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
10139N/A Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
10139N/A Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
10139N/A Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
10139N/A LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi"),
10139N/A "OFCLASS(?'a, pcpo_class) ==> OFCLASS(?'a, Joker_class)"),
10139N/A "fix$Prelude_MPList_copy$?x = ?x"),
10139N/A "fix$Prelude_MyList_copy$?x = ?x"),
10139N/A "Red == LAM a. Prelude_Color_abs$(sinl$a)"),
10139N/A "Prelude_Color_rep$(Prelude_Color_abs$?x) = ?x"),
10139N/A "Prelude_Color_abs$(Prelude_Color_rep$?x) = ?x"),
10139N/A "Blue == LAM a. Prelude_Color_abs$(sinr$a)"),
10139N/A Prelude_Color_when$(LAM a. sinl$a)$(LAM a. sinr$a)"),
10139N/A "Prelude_Color_take == %n. iterate n Prelude_Color_copy UU"),
10139N/A LAM f1 f2 x. sscase$f1$f2$(Prelude_Color_rep$x)"),
10139N/A "Prelude_MPList_rep$(Prelude_MPList_abs$?x) = ?x"),
10139N/A "Prelude_MPList_abs$(Prelude_MPList_rep$?x) = ?x"),
10139N/A "Prelude_MyList_rep$(Prelude_MyList_abs$?x) = ?x"),
10139N/A "Prelude_MyList_abs$(Prelude_MyList_rep$?x) = ?x"),
10139N/A "Red_1 == Prelude_Color_when$(LAM a. a)$UU"),
10139N/A (EX a. a ~= UU & x = Red$a & x' = Red$a) |
10139N/A (EX a. a ~= UU & x = Blue$a & x' = Blue$a)"),
10139N/A Prelude_MPList_when$(sinl$ONE)$(LAM a b P'.
10139N/A "Prelude_MPList_take == %n. iterate n Prelude_MPList_copy UU"),
10139N/A ssplit$(f2$a)))$(Prelude_MPList_rep$x)"),
10139N/A Prelude_MyList_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),
11904N/A "Prelude_MyList_take == %n. iterate n Prelude_MyList_copy UU"),
sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_MyList_rep$x)"),
"Blue_1 == Prelude_Color_when$UU$(LAM a. a)"),
"Prelude_Color_finite == %x. EX n. Prelude_Color_take n$x = x"),
"is_Red == Prelude_Color_when$(LAM a. TT)$(LAM a. FF)"),
"MPNil == Prelude_MPList_abs$(sinl$ONE)"),
R P' P'' & x = MPCons$a$b$P' & x' = MPCons$a$b$P'')"),
"MyNil == Prelude_MyList_abs$(sinl$ONE)"),
R P' P'' & x = MyCons$a$P' & x' = MyCons$a$P'')"),
"is_Blue == Prelude_Color_when$(LAM a. FF)$(LAM a. TT)"),
"MPCons == LAM a b P'. Prelude_MPList_abs$(sinr$(:a, b, P':))"),
"Prelude_MPList_finite == %x. EX n. Prelude_MPList_take n$x = x"),
"MyCons == LAM a P'. Prelude_MyList_abs$(sinr$(:a, P':))"),
"Prelude_MyList_finite == %x. EX n. Prelude_MyList_take n$x = x"),
"match_Red == Prelude_Color_when$(LAM a. return$a)$(LAM a. fail)"),
"methodTwo == default__methodTwo"),
"MPCons_1 == Prelude_MPList_when$UU$(LAM a b P'. a)"),
"MPCons_2 == Prelude_MPList_when$UU$(LAM a b P'. b)"),
"MPCons_3 == Prelude_MPList_when$UU$(LAM a b P'. P')"),
"is_MPNil == Prelude_MPList_when$TT$(LAM a b P'. FF)"),
"MyCons_1 == Prelude_MyList_when$UU$(LAM a P'. a)"),
"MyCons_2 == Prelude_MyList_when$UU$(LAM a P'. P')"),
"is_MyNil == Prelude_MyList_when$TT$(LAM a P'. FF)"),
"match_Blue == Prelude_Color_when$(LAM a. fail)$(LAM a. return$a)"),
"is_MPCons == Prelude_MPList_when$FF$(LAM a b P'. TT)"),
"methodOne == default__methodOne"),
"methodTwo == default__methodTwo"),
"is_MyCons == Prelude_MyList_when$FF$(LAM a P'. TT)"),
If (LAM x y. Def (x = y))$y$TT then Red$x else Blue$x fi"),
Prelude_MPList_when$(return$())$(LAM a b P'. fail)"),
"match_MyNil == Prelude_MyList_when$(return$())$(LAM a P'. fail)"),
Prelude_MPList_when$fail$(LAM a b P'. return$<a, b, P'>)"),
Prelude_MyList_when$fail$(LAM a P'. return$<a, P'>)")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "ex_fibon_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "ex_fibon_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
If (LAM x y. Def (x = y))$n$(Def 0)
else If (LAM x y. Def (x = y))$n$(Def 1)
op -$n$(Def 2))) fi fi))")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "ex_let_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "ex_let_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
let testName1 >>= myEqual$a$b
in Let (myEqual$b$c) (Rep_CFun (trand$testName1))"),
LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "ex_list_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "ex_list_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
| lCons$pX1$pX2 => lCons$(f$pX1)$(myMap$pX2$f)))"),
If (LAM x y. Def (x = y))$x$(lCons$(lHd$x)$(lTl$y))
then TT else FF fi")] : (string *
Thm.thm) list
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "ex_mutrec_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "ex_mutrec_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
If (LAM x y. Def (x = y))$n$(Def 0)
else If (LAM x y. Def (x = y))$n$(Def 1)
op -$n$(Def 2))) fi fi))"),
LAM x y. If (LAM x y. Def (x = y))$x$y then TT else FF fi"),
then Red$((LAM z. Square$x$z)$x)
else Blue$(Rectangle$x$y) fi"),
cfst$(FIX <mRecFun1, mRecFun2>.
If (LAM x y. Def (x = y))$n$(Def 0)
else If (LAM x y. Def (x = y))$n$(Def 1)
op -$n$(Def 2))) fi fi)),
If (LAM x y. Def (x = y))$n$(Def 0)
else If (LAM x y. Def (x = y))$n$(Def 1)
op -$n$(Def 1))) fi fi))>)"),
csnd$(FIX <mRecFun1, mRecFun2>.
If (LAM x y. Def (x = y))$n$(Def 0)
else If (LAM x y. Def (x = y))$n$(Def 1)
op -$n$(Def 2))) fi fi)),
If (LAM x y. Def (x = y))$n$(Def 0)
else If (LAM x y. Def (x = y))$n$(Def 1)
op -$n$(Def 1))) fi fi))>)"),
"cfst$(fix$Prelude_CList_Prelude_LColor_copy)$?x1.0 = ?x1.0"),
"Prelude_Form_rep$(Prelude_Form_abs$?x) = ?x"),
"Prelude_Form_abs$(Prelude_Form_rep$?x) = ?x"),
"csnd$(fix$Prelude_CList_Prelude_LColor_copy)$?x2.0 = ?x2.0"),
"fix$Prelude_MyList_copy$?x = ?x"),
"Prelude_CList_rep$(Prelude_CList_abs$?x) = ?x"),
"Prelude_CList_abs$(Prelude_CList_rep$?x) = ?x"),
Prelude_Form_when$(LAM a b.
sinl$(:a, b:))$(LAM a b. sinr$(:a, b:))"),
"Prelude_Form_take == %n. iterate n Prelude_Form_copy UU"),
sscase$(ssplit$f1)$(ssplit$f2)$(Prelude_Form_rep$x)"),
Prelude_CList_when$(sinl$ONE)$(LAM P'1 P'2.
sinr$(:P'1, cfst$f$P'2:))"),
%n. cfst$(iterate n Prelude_CList_Prelude_LColor_copy UU)"),
sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_CList_rep$x)"),
a ~= UU & b ~= UU & x = Square$a$b & x' = Square$a$b) |
b ~= UU & x = Rectangle$a$b & x' = Rectangle$a$b)"),
"Red == LAM a. Prelude_LColor_abs$(sinr$(sinl$a))"),
"Prelude_LColor_rep$(Prelude_LColor_abs$?x) = ?x"),
"Prelude_LColor_abs$(Prelude_LColor_rep$?x) = ?x"),
"Prelude_MyList_rep$(Prelude_MyList_abs$?x) = ?x"),
"Prelude_MyList_abs$(Prelude_MyList_rep$?x) = ?x"),
"CCons == LAM P'1 P'2. Prelude_CList_abs$(sinr$(:P'1, P'2:))"),
"Trans == Prelude_CList_abs$(sinl$ONE)"),
"Square == LAM a b. Prelude_Form_abs$(sinl$(:a, b:))"),
"Prelude_Form_finite == %x. EX n. Prelude_Form_take n$x = x"),
"Blue == LAM a. Prelude_LColor_abs$(sinl$a)"),
Prelude_LColor_when$(LAM a.
sinl$a)$(LAM a. sinr$(sinl$a))$(LAM P'. sinr$(sinr$P'))"),
%n. csnd$(iterate n Prelude_CList_Prelude_LColor_copy UU)"),
sscase$f1$(sscase$f2$f3)$(Prelude_LColor_rep$x)"),
Prelude_MyList_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),
"Prelude_MyList_take == %n. iterate n Prelude_MyList_copy UU"),
sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_MyList_rep$x)"),
"Prelude_CList_finite == %x1. EX n. Prelude_CList_take n$x1 = x1"),
"Multi == LAM P'. Prelude_LColor_abs$(sinr$(sinr$P'))"),
"Red_1 == Prelude_LColor_when$UU$(LAM a. a)$UU"),
"MyNil == Prelude_MyList_abs$(sinl$ONE)"),
R P' P'' & x = MyCons$a$P' & x' = MyCons$a$P'')"),
"CCons_1 == Prelude_CList_when$UU$(LAM P'1 P'2. P'1)"),
"CCons_2 == Prelude_CList_when$UU$(LAM P'1 P'2. P'2)"),
"Square_1 == Prelude_Form_when$(LAM a b. a)$UU"),
"Square_2 == Prelude_Form_when$(LAM a b. b)$UU"),
"Blue_1 == Prelude_LColor_when$(LAM a. a)$UU$UU"),
"Prelude_LColor_finite ==
%x2. EX n. Prelude_LColor_take n$x2 = x2"),
Prelude_LColor_when$(LAM a. FF)$(LAM a. TT)$(LAM P'. FF)"),
"MyCons == LAM a P'. Prelude_MyList_abs$(sinr$(:a, P':))"),
"Prelude_MyList_finite == %x. EX n. Prelude_MyList_take n$x = x"),
"is_CCons == Prelude_CList_when$FF$(LAM P'1 P'2. TT)"),
"is_Trans == Prelude_CList_when$TT$(LAM P'1 P'2. FF)"),
"Rectangle == LAM a b. Prelude_Form_abs$(sinr$(:a, b:))"),
"is_Square == Prelude_Form_when$(LAM a b. TT)$(LAM a b. FF)"),
"Multi_1 == Prelude_LColor_when$UU$UU$(LAM P'. P')"),
Prelude_LColor_when$(LAM a. TT)$(LAM a. FF)$(LAM P'. FF)"),
Prelude_LColor_when$(LAM a. FF)$(LAM a. FF)$(LAM P'. TT)"),
"MyCons_1 == Prelude_MyList_when$UU$(LAM a P'. a)"),
"MyCons_2 == Prelude_MyList_when$UU$(LAM a P'. P')"),
"is_MyNil == Prelude_MyList_when$TT$(LAM a P'. FF)"),
"Rectangle_1 == Prelude_Form_when$UU$(LAM a b. a)"),
"Rectangle_2 == Prelude_Form_when$UU$(LAM a b. b)"),
Prelude_LColor_when$(LAM a.
fail)$(LAM a. return$a)$(LAM P'. fail)"),
"is_MyCons == Prelude_MyList_when$FF$(LAM a P'. TT)"),
Prelude_CList_when$fail$(LAM P'1 P'2. return$<P'1, P'2>)"),
Prelude_CList_when$(return$())$(LAM P'1 P'2. fail)"),
"is_Rectangle == Prelude_Form_when$(LAM a b. FF)$(LAM a b. TT)"),
Prelude_Form_when$(LAM a b. return$<a, b>)$(LAM a b. fail)"),
Prelude_LColor_when$(LAM a.
return$a)$(LAM a. fail)$(LAM P'. fail)"),
Prelude_LColor_when$(LAM a.
fail)$(LAM a. fail)$(LAM P'. return$P')"),
"match_MyNil == Prelude_MyList_when$(return$())$(LAM a P'. fail)"),
Prelude_MyList_when$fail$(LAM a P'. return$<a, P'>)"),
Prelude_Form_when$(LAM a b. fail)$(LAM a b. return$<a, b>)"),
"Prelude_CList_Prelude_LColor_copy ==
LAM f. <Prelude_CList_copy$f, Prelude_LColor_copy$f>"),
"Prelude_CList_Prelude_LColor_bisim ==
x1 = Trans & x1' = Trans |
x1 = CCons$P'1$P'2 & x1' = CCons$P'1$P'2')) &
(EX a. a ~= UU & x2 = Blue$a & x2' = Blue$a) |
(EX a. a ~= UU & x2 = Red$a & x2' = Red$a) |
(EX P'. P' ~= UU & x2 = Multi$P' & x2' = Multi$P'))")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "incmpl_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "incmpl_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
"Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),
"SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),
"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),
"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),
"Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),
"Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),
"Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),
Prelude_Natx_when$(sinl$ONE)$(LAM a.
sinr$(sinl$a))$(LAM P'1 P'2.
sinr$(sinr$(:f$P'1, P'2:)))"),
"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),
f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),
"Minx == Prelude_Boolx_abs$(sinl$ONE)"),
Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),
"Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),
case Prelude_Boolx_rep$x of sinl$dummy => f1
"SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),
"SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),
(EX a. a ~= UU & x = Sx$a & x' = Sx$a) |
R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),
"is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),
"is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),
"Plusx == Prelude_Boolx_abs$(sinr$ONE)"),
x = Minx & x' = Minx | x = Plusx & x' = Plusx"),
"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),
"is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),
"Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),
"is_Minx == Prelude_Boolx_when$TT$FF"),
Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),
Prelude_Natx_when$(return$())$(LAM a.
fail)$(LAM P'1 P'2. fail)"),
"is_Plusx == Prelude_Boolx_when$FF$TT"),
Prelude_Natx_when$fail$(LAM a.
fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),
"match_Minx == Prelude_Boolx_when$(return$())$fail"),
"match_Plusx == Prelude_Boolx_when$fail$(return$())")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "mrec3_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "mrec3_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
| SSx$pX1$pX2 => map2$pX1$pX2$f)),
| Sx$pX1 => Sx$(fliftbin op +$pX1$(Def 1))
If (LAM x y. Def (x = y))$pX2$Minx
then SSx$pX1$w else map1$pX1$f fi))>)"),
case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
| SSx$pX1$pX2 => map2$pX1$pX2$f)),
| Sx$pX1 => Sx$(fliftbin op +$pX1$(Def 1))
If (LAM x y. Def (x = y))$pX2$Minx
then SSx$pX1$w else map1$pX1$f fi))>)"),
"Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),
"SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),
"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),
"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),
"Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),
"Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),
"Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),
Prelude_Natx_when$(sinl$ONE)$(LAM a.
sinr$(sinl$a))$(LAM P'1 P'2.
sinr$(sinr$(:f$P'1, P'2:)))"),
"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),
f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),
"Minx == Prelude_Boolx_abs$(sinl$ONE)"),
Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),
"Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),
case Prelude_Boolx_rep$x of sinl$dummy => f1
"SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),
"SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),
(EX a. a ~= UU & x = Sx$a & x' = Sx$a) |
R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),
"is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),
"is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),
"Plusx == Prelude_Boolx_abs$(sinr$ONE)"),
x = Minx & x' = Minx | x = Plusx & x' = Plusx"),
"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),
"is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),
"Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),
"is_Minx == Prelude_Boolx_when$TT$FF"),
Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),
Prelude_Natx_when$(return$())$(LAM a.
fail)$(LAM P'1 P'2. fail)"),
"is_Plusx == Prelude_Boolx_when$FF$TT"),
Prelude_Natx_when$fail$(LAM a.
fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),
"match_Minx == Prelude_Boolx_when$(return$())$fail"),
"match_Plusx == Prelude_Boolx_when$fail$(return$())")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "mrec_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
case x of Zx => <Zx, Def 0>
<Sx$pX1$(cfst$(fun1$pX2)),
fliftbin op *$pX1$(fun2$pX2)>)),
fliftbin op +$(csnd$(fun1$pX2))$pX1))>)"),
case x of Zx => <Zx, Def 0>
<Sx$pX1$(cfst$(fun1$pX2)),
fliftbin op *$pX1$(fun2$pX2)>)),
fliftbin op +$(csnd$(fun1$pX2))$pX1))>)"),
"Sx == LAM a P'. Prelude_Natx_abs$(sinr$(:a, P':))"),
"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),
"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),
"Sx_1 == Prelude_Natx_when$UU$(LAM a P'. a)"),
"Sx_2 == Prelude_Natx_when$UU$(LAM a P'. P')"),
Prelude_Natx_when$(sinl$ONE)$(LAM a P'. sinr$(:a, f$P':))"),
"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),
sscase$(LAM dummy. f1)$(ssplit$f2)$(Prelude_Natx_rep$x)"),
P'' ~= UU & R P' P'' & x = Sx$a$P' & x' = Sx$a$P'')"),
"is_Sx == Prelude_Natx_when$FF$(LAM a P'. TT)"),
"is_Zx == Prelude_Natx_when$TT$(LAM a P'. FF)"),
"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),
"match_Sx == Prelude_Natx_when$fail$(LAM a P'. return$<a, P'>)"),
"match_Zx == Prelude_Natx_when$(return$())$(LAM a P'. fail)")]
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=30000K,ib=6000K,ip=100%,mb=10096K,mp=20%)
Loading theory "HsHOLCF" (required by "wcard_hc")
fliftbin :: "('a => 'b => 'c) => 'a lift -> 'b lift -> 'c lift"
Loading theory "wcard_hc"
sig val initialize : string list -> unit val record : string -> unit end
{ProtoPure, Pure, CPure, HOL, Lattice_Locales, Orderings, LOrder, Set,
Typedef, Fun, Product_Type, FixedPoint, Sum_Type, Relation, Record,
Inductive, Transitive_Closure, Wellfounded_Recursion, OrderedGroup,
Ring_and_Field, Nat, NatArith, Datatype_Universe, Datatype, Divides,
Power, Finite_Set, Wellfounded_Relations, Equiv_Relations, IntDef,
Numeral, IntArith, SetInterval, Recdef, IntDiv, NatBin, NatSimprocs,
Presburger, Relation_Power, Parity, GCD, Binomial, PreList, List, Map,
Refute, SAT, Hilbert_Choice, Infinite_Set, Extraction, Reconstruction,
Main, Porder, Pcpo, Ffun, Cont, Adm, Pcpodef, Cfun, Cprod, Sprod, Ssum,
Up, Discrete, Lift, One, Tr, Fix, Fixrec, Domain, HOLCF, HsHOLCF,
case x of Zx => Sx$(f$(Def 0)) | Sx$pX1 => Sx$(f$pX1)
"Sx == LAM a. Prelude_Natx_abs$(sinr$(sinl$a))"),
"SSx == LAM P'1 P'2. Prelude_Natx_abs$(sinr$(sinr$(:P'1, P'2:)))"),
"Prelude_Natx_rep$(Prelude_Natx_abs$?x) = ?x"),
"Prelude_Natx_abs$(Prelude_Natx_rep$?x) = ?x"),
"Prelude_Boolx_rep$(Prelude_Boolx_abs$?x) = ?x"),
"Prelude_Boolx_abs$(Prelude_Boolx_rep$?x) = ?x"),
"Sx_1 == Prelude_Natx_when$UU$(LAM a. a)$UU"),
Prelude_Natx_when$(sinl$ONE)$(LAM a.
sinr$(sinl$a))$(LAM P'1 P'2.
sinr$(sinr$(:f$P'1, P'2:)))"),
"Prelude_Natx_take == %n. iterate n Prelude_Natx_copy UU"),
f1)$(sscase$f2$(ssplit$f3))$(Prelude_Natx_rep$x)"),
"Minx == Prelude_Boolx_abs$(sinl$ONE)"),
Prelude_Boolx_when$(sinl$ONE)$(sinr$ONE)"),
"Prelude_Boolx_take == %n. iterate n Prelude_Boolx_copy UU"),
case Prelude_Boolx_rep$x of sinl$dummy => f1
"SSx_1 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'1)"),
"SSx_2 == Prelude_Natx_when$UU$UU$(LAM P'1 P'2. P'2)"),
(EX a. a ~= UU & x = Sx$a & x' = Sx$a) |
R P'1 P'1' & x = SSx$P'1$P'2 & x' = SSx$P'1'$P'2)"),
"is_Sx == Prelude_Natx_when$FF$(LAM a. TT)$(LAM P'1 P'2. FF)"),
"is_Zx == Prelude_Natx_when$TT$(LAM a. FF)$(LAM P'1 P'2. FF)"),
"Plusx == Prelude_Boolx_abs$(sinr$ONE)"),
x = Minx & x' = Minx | x = Plusx & x' = Plusx"),
"Prelude_Natx_finite == %x. EX n. Prelude_Natx_take n$x = x"),
"is_SSx == Prelude_Natx_when$FF$(LAM a. FF)$(LAM P'1 P'2. TT)"),
"Prelude_Boolx_finite == %x. EX n. Prelude_Boolx_take n$x = x"),
"is_Minx == Prelude_Boolx_when$TT$FF"),
Prelude_Natx_when$fail$(LAM a. return$a)$(LAM P'1 P'2. fail)"),
Prelude_Natx_when$(return$())$(LAM a.
fail)$(LAM P'1 P'2. fail)"),
"is_Plusx == Prelude_Boolx_when$FF$TT"),
Prelude_Natx_when$fail$(LAM a.
fail)$(LAM P'1 P'2. return$<P'1, P'2>)"),
"match_Minx == Prelude_Boolx_when$(return$())$fail"),
"match_Plusx == Prelude_Boolx_when$fail$(return$())")]