43b4c41fbb07705c9df321221ab9cb9832460407Christian Maedertype bool ::= True |

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder False

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederop a : bool = (op True : bool) as bool

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederop notA : bool

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder = case (op a : bool) of

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (op True : bool) -> (op False : bool) |

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (op False : bool) -> (op True : bool)

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder as bool

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederop b : bool

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder = let (var x : bool) = (op True : bool);

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder (var y : bool) = (op False : bool);

f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder (var z : bool) = (var x : bool)

c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder in (op True : bool)

c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder as bool

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederop b : bool -> bool

68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder = \ (var x : bool) .! (var x : bool) as bool -> bool

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder%% Type Constructors -----------------------------------------------------

01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder? : +Type -> Type

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till MossakowskiLogical : Type := ? Unit

9dac90ec2be2a72e03893095461960d483fe2fc2Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

5e5d3e82af3bc2834f8718a52d9f45da80220273Dominik LueckeUnit : Type

124c859ba4741d5e36d5d98634886b430b7af093Christian Maeder__*__ : +Type -> +Type -> Type

ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski__*__*__ : +Type -> +Type -> +Type -> Type

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder__->?__ : -Type -> +Type -> Type

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichbool

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder : Type

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder %[type bool

4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder ::= True : bool

4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder False : bool]%

8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder%% Assumptions -----------------------------------------------------------

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichFalse : bool %(construct bool)%

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederTrue : bool %(construct bool)%

74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedera : bool %(op)% = (op True : bool) as bool

f38b3687c5558128515e34fb85d8b466d22dc300Christian Maederb : bool -> bool

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder %(op)% = \ (var x : bool) .! (var x : bool) as bool -> bool

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder : bool

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder %(op)%

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder = let (var x : bool) = (op True : bool);

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder (var y : bool) = (op False : bool);

f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder (var z : bool) = (var x : bool)

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder in (op True : bool)

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder as bool

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederbottom : forall a : Type . a %(fun)%

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

c3053d57f642ca507cdf79512e604437c4546cb9Christian Maederfalse : Unit %(fun)%

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maedernot__ : ? Unit ->? Unit %(fun)%

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaedernotA

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder : bool

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder %(op)%

d0279930f87bf39843e0bd2992a4789322662144Christian Maeder = case (op a : bool) of

8be81a0578b59f08641da7fad1479e1f9e83c6e9Kristina Sojakova (op True : bool) -> (op False : bool) |

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (op False : bool) -> (op True : bool)

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder as bool

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maedertrue : Unit %(fun)%

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder�__ : ? Unit ->? Unit %(fun)%

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder%% Sentences -------------------------------------------------------------

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maedertype bool

8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder ::= True : bool

456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder False : bool %(ga_bool)%

d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maedera = (True as bool) %(def_a)%

23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian MaedernotA =

23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder(case a of

8cacad2a09782249243b80985f28e9387019fe40Christian Maeder True -> False |

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder False -> True

a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder as bool) %(def_notA)%

363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder(op b : bool) =

8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder(let x = True;

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich y = False;

4e23d551da8fb051cc4752319740ae7858ef1044Christian Maeder z = x

797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder in True

431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder as bool) %(def_b)%

f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder(op b : bool -> bool) = (\ x .! x as bool -> bool) %(def_b)%

498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder