:: deftheorem defines TrivialCTLModel MODELC_1:def 30 :
TrivialCTLModel = CTLModelStr(# {0},([#] {0}),op2,op1,op1,op1,op2 #);