:: deftheorem defines BASSModel MODELC_1:def 58 :
for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S) holds BASSModel (R,BASSIGN) = CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #);