afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart Poetteringclass Type

c343be283b7152554bac0c02493a4e1759c163f7Kay Sievers

b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-Szmekvar t:Type

b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-Szmek

f957632b960a0a42999b38ded7089fa602b41745Kay Sieversclass TYPE : {x.x < t}

f957632b960a0a42999b38ded7089fa602b41745Kay Sievers

f957632b960a0a42999b38ded7089fa602b41745Kay Sieverstype Pred __ : Type- -> Type; Unit:TYPE

f957632b960a0a42999b38ded7089fa602b41745Kay Sievers

a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poettering

20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sieversclass a, b, c

afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart Poetteringclass a, b, c <d; a:b

d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmek

d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmektype s:c

d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmek

d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmekpred tt : s

d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmekvar x : s

3f85ef0f05ffc51e19f86fb83a1c51e8e3cd6817Harald Hoyer

afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart Poetteringprogram tt = \x: s . ()

afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart Poettering

afea8d3853d0f76b3845729ff00e75d281f43a1bZbigniew Jędrzejewski-Szmekprogram __res__ (x: s, y: t) : s = x ;

f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringfst (x: s, y: t) : s = x ;

f85857df75cfedbc0d10b8ca2400188dc8f4c22eLennart Poetteringsnd (x: s, y: t) : t = y

f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering

bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poetteringpred eq : s * s

f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering

bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poetteringtype s < ?s

81429136905a6204875174b60a179333b7f3c9e4Kay Sievers

e7b4d43ec3d5eb0099a3978f98a46f3c15443b23Lennart Poetteringprogram all (p: (?s)) : (?Unit) = eq(p, tt)

58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poettering

58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poetteringprogram And (x, y: (?Unit)) :(?Unit) = t1() res t2()

83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmek

83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmekprogram __impl__ (x, y: (?Unit)) = eq(x, x And y)

83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmek

83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmekprogram __or__ (x, y: (?Unit)) :(?Unit) = all(\r: (?Unit).

83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmek ((x impl r) res (y impl r)) impl r)

81429136905a6204875174b60a179333b7f3c9e4Kay Sievers

fbe1a1a94f19112d7e5d60c40d87487ad24e2ce4Lennart Poettering; ex (p: (?s)) :(?Unit) = all(\r: (?Unit).

6c78f43c7b0e54e695af49917fda79b584f46830Lennart Poettering all(\x:s. p(x) impl r) impl r)

6c78f43c7b0e54e695af49917fda79b584f46830Lennart Poettering

7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering; ff () :(?Unit) = all(\r: (?Unit). r())

7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering

7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering;

7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering

7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering

b568ef14a75dffb7182e0acbdec743b31df2a597Lennart Poetteringforall x: t; y : t

c2d5b3c94d0c082ef29597fb230f8b88b124bab8Lennart Poettering%(..)%

264b8070715d2d19344c4991ace21147d998f56dLennart Poettering. x = y

264b8070715d2d19344c4991ace21147d998f56dLennart Poettering

4ecd22142543aac55ddac1da3b7d6882c009d637Lennart Poettering%[% [ ] % %[

4ecd22142543aac55ddac1da3b7d6882c009d637Lennart Poettering]%

7e27f3121e5a10629302b5221eb21345f832724aLennart Poettering%[ ]%

7e27f3121e5a10629302b5221eb21345f832724aLennart Poettering]%

f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering

f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering%[ ]%

d48b7bd271b1e70924c8485d2f95c2f5a1ae77cbLennart Poettering

d48b7bd271b1e70924c8485d2f95c2f5a1ae77cbLennart Poettering

25e14499c4c5b02229d05a5bc26c3693ade5f987Lennart Poettering sort s

25e14499c4c5b02229d05a5bc26c3693ade5f987Lennart Poettering op a: (?s); %[ Should be: op a:?s ]%

758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering

758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering type Data1 ::= a | b | c;

821cc13ddae40fb7608458b44aaa7a3fd33d56d9Lennart Poettering type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1

821cc13ddae40fb7608458b44aaa7a3fd33d56d9Lennart Poettering type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?

8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringData1)

8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:?Data1)?

8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering

8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poetteringaxioms true ;forall x:s.e;

8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poetteringforall x:s.e

8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering