equal
deleted
inserted
replaced
52 |
52 |
53 (* this means that for nil and UU the effect is unpredictable *) |
53 (* this means that for nil and UU the effect is unpredictable *) |
54 Init_def |
54 Init_def |
55 "Init P s == (P (unlift (HD`s)))" |
55 "Init P s == (P (unlift (HD`s)))" |
56 |
56 |
57 |
|
58 (* FIX: Introduce nice symbol infix suntax *) |
|
59 suffix_def |
57 suffix_def |
60 "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" |
58 "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" |
61 |
59 |
62 (* FIX: Introduce nice symbol infix suntax *) |
|
63 tsuffix_def |
60 tsuffix_def |
64 "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s" |
61 "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s" |
65 |
62 |
66 Box_def |
63 Box_def |
67 "([] P) s == ! s2. tsuffix s2 s --> P s2" |
64 "([] P) s == ! s2. tsuffix s2 s --> P s2" |
68 |
65 |
69 Next_def |
66 Next_def |
70 "(Next P) s == if TL`s=UU then (P s) else P (TL`s)" |
67 "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)" |
71 |
68 |
72 Diamond_def |
69 Diamond_def |
73 "<> P == .~ ([] (.~ P))" |
70 "<> P == .~ ([] (.~ P))" |
74 |
71 |
75 Leadsto_def |
72 Leadsto_def |