020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettich

020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettichlibrary SyntaxTest

020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettich

020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettichlogic CASL_DL

020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettich

cbea3f4c0de14871391f2e9f308e705ef0039eedKlaus Luettichspec X0 = {}

cbea3f4c0de14871391f2e9f308e705ef0039eedKlaus Luettich

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettichspec X1 =

020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettich sort T1,T2,T3 < Thing

020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettich pred R1 : T1 * T2

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich pred R1 : Thing * Thing

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich op i1 : T2

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich forall x : T1

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . x in T3 <=> minCardinality[(pred R1: T1 * T2)](x,10)

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . forall x : Thing

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . x in T3 <=> minCardinality[R1](x,3)

478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . R1(x as T1,i1)

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettichend

0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich

2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettichspec X2 =

2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich sort S1 < Thing

2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich pred R : S1 * Thing

2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich forall x : S1

2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich . x in S1 <=> cardinality[R](x,2)

2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich

ea6f4edb6ecdefe4bbe700b8bdc93942c95feaf8Klaus Luettich