faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poetteringlogic ExtModal

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poetteringspec Try2 =

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering time modality t

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering modalities a,b

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering sort N

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering flexible op s__: N -> N

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering flexible ops 0,1: N

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering . [a] >= 2 (not (s 0 = 1)) U X X true

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering . <(a)> <= 00 false S (X true U Y true)

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering . < > <=1 true U <> <=1 true

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering . <true?> <=1 true

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering . mu b. true %implied

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poetteringend

faae655de3cdbed4be1d472b01ce0c4d81e905edLennart Poettering