c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Lueckespec CardinalityRestrictions =
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke Nat with Nat |-> nonNegativeInteger
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke sort gn_Object, gn_Subject
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke generated type gn_Set[gn_Object] ::= gn_eset | gn_insert (gn_Set[gn_Object];gn_Object)
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke pred gn_contained: gn_Object * gn_Set[gn_Object]
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke op gn_card __ : gn_Set[gn_Object] -> nonNegativeInteger
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke pred gn_predicate: gn_Subject * gn_Object
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke ops gn_setOfPred[gn_predicate] __ : gn_Subject ->? gn_Set[gn_Object]
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke forall gn_x, gn_y : gn_Object; gn_M, gn_N : gn_Set[gn_Object]
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke . not (gn_contained (gn_x, gn_eset))
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke . gn_contained (gn_x, (gn_insert (gn_M, gn_y))) <=> gn_x = gn_y \/ gn_contained (gn_x, gn_M)
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke . gn_M = gn_N <=> (forall gn_z: gn_Object. gn_contained (gn_z, gn_M) <=> gn_contained (gn_z, gn_N))
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke . gn_card (gn_eset) = 0
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke . gn_card (gn_insert (gn_M, gn_x)) = gn_card (gn_M) when gn_contained (gn_x, gn_M) else suc(gn_card(gn_M))
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke forall x : gn_Subject . def gn_setOfPred[gn_predicate](x) <=> exists s : gn_Set[gn_Object]. forall y : gn_Object . gn_predicate (x, y) <=> gn_contained (y, s)
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke forall x : gn_Subject . def gn_setOfPred[gn_predicate](x) => forall y: gn_Object. gn_predicate(x, y) <=> gn_contained (y, gn_setOfPred[gn_predicate] (x))
c8fc9f576cc6a21277315fec0fe88e24d2c43374Dominik Luecke forall x : gn_Subject . gn_card (gn_setOfPred[gn_predicate] (x)) = 9
72f39d07062c0e584ce75597364a726917f345eaDominik Luecke forall x : gn_Subject . def gn_setOfPred[gn_predicate](x) => gn_card (gn_setOfPred[gn_predicate] (x)) >= 9