020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettichlibrary SyntaxTest
c827fed2bb995225b7b19eb673a40e207adf4bf6Klaus Luettich sort T1,T2, T3
020292f4a997a0c012b687fed94c3bbdae5213d5Klaus Luettich pred R1 : T1 * T2
478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich pred R1 : Thing * Thing
478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich forall x : T1
478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . x in T3 <=> minCardinality[(pred R1: T1 * T2)](x,10)
478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . forall x : Thing
8d806c1392e09b4ac2917a7b536e390fcf1d6265Dominik Luecke . x in T3 <=> minCardinality[R1](x,3,T1)
478b48030a6cbdefc35ddd31d5ccb0357331b6ddKlaus Luettich . R1(x as T1,i1)
2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich pred R : S1 * Thing
2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich forall x : S1
2033aff510a8af9722ea9928d5b10785c802ff0cKlaus Luettich . x in S1 <=> cardinality[R](x,2)
c827fed2bb995225b7b19eb673a40e207adf4bf6Klaus Luettich sort C1, C2 < C3
c827fed2bb995225b7b19eb673a40e207adf4bf6Klaus Luettich sort X < X1; X < X2; X2 < X5