499b34cea04a46823d003d4c0520c8b03e8513cbBrian Wellington

816e576f77e2c46df3e3d97d65822aa8aded7c4bDavid Lawrencelibrary SyntaxTest

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafsson

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafssonlogic CASL_DL

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafsson

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafssonspec X0 = {}

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafsson

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafssonspec X1 =

1b855974958ebca91882c4b59f66c48dd5784b87Andreas Gustafsson sort T1,T2,T3 < Thing

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson pred R1 : T1 * T2

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson pred R1 : Thing * Thing

181232550d33f7d7846cdc08e1da01f0972c15d6Andreas Gustafsson op i1 : T2

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson forall x : T1

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

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson . forall x : Thing

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson . x in T3 <=> minCardinality[R1](x,3)

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson . R1(x as T1,i1)

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafssonend

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson

abea3fdc7fafcadf4275a14f261ad6e2332cace4Andreas Gustafsson