:: deftheorem defines TrivialLTLModel MODELC_2:def 31 :
TrivialLTLModel = LTLModelStr(# {0},([#] {0}),op2,op2,op1,op1,op2,op2 #);