theorem Th12: :: MODELC_2:12

for F, G being LTL-formula holds
( ('not' F) . 1 = 0 & (F '&' G) . 1 = 1 & (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )