a030fdd60d67ac5b7fe898c4346a64f136807013Christian Maederclass TYPE < Type
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maedertype Pred __ : -Type -> Type; Unit:TYPE
9b3f1a9c8994dc5a964d53de628f650317fa6d6fChristian Maederclass a, b, c <d; a<b
9b3f1a9c8994dc5a964d53de628f650317fa6d6fChristian Maederprogram tt = \x: s . ()
aa60342b6a000c6798730e1b1ddeec846254c62cChristian Maederprogram __res__ (x: s, y: t) : s = x ;
9b3f1a9c8994dc5a964d53de628f650317fa6d6fChristian Maederfst (x: s, y: t) : s = x ;
9b3f1a9c8994dc5a964d53de628f650317fa6d6fChristian Maedersnd (x: s, y: t) : t = y
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maederpred eq : s * s
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maederprogram all (p: (?s)) : (?Unit) = eq(p, tt)
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maederprogram And (x, y: (?Unit)) :(?Unit) = t1() res t2()
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maederprogram __impl__ (x, y: (?Unit)) = eq(x, x And y)
9b3f1a9c8994dc5a964d53de628f650317fa6d6fChristian Maederprogram __or__ (x, y: (?Unit)) :(?Unit) = all(\r: (?Unit).
7b47917488ffdd72119358c064c94e5dfc4f8fe3Christian Maeder ((x impl r) res (y impl r)) impl r)
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder; ex (p: (?s)) :(?Unit) = all(\r: (?Unit).
7b47917488ffdd72119358c064c94e5dfc4f8fe3Christian Maeder all(\x:s. p(x) impl r) impl r)
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder; ff () :(?Unit) = all(\r: (?Unit). r())
9b3f1a9c8994dc5a964d53de628f650317fa6d6fChristian Maederforall x: t; y : t
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maeder op a: (?s); %[ Should be: op a:?s ]%
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maeder type Data1 ::= a | b | c;
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maeder type Data2 ::= Cons21 (Data1; Data2) | Cons22(Data2; Data1) | sort Data1
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maeder type Data3 ::= Cons31 (sel1:?Data1; sel2:?Data2) | Cons32(sel2:?Data2; sel1:?
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maeder type Data4 ::= Cons41 (sel1:?Data1; sel2:?Data2)? | Cons42(sel2:?Data2; sel1:?Data1)?
5214cf3742dc626a7efc5ec851db09bf0ff1f579Christian Maederaxioms true ;forall x:s.e;