equal
deleted
inserted
replaced
114 & Min <= n & n <= Max}" |
114 & Min <= n & n <= Max}" |
115 |
115 |
116 |
116 |
117 Lprg :: state program |
117 Lprg :: state program |
118 (*for the moment, we OMIT button_press*) |
118 (*for the moment, we OMIT button_press*) |
119 "Lprg == mk_program (UNIV, |
119 "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s & |
120 {s. floor s = Min & ~ up s & move s & stop s & |
|
121 ~ open s & req s = {}}, |
120 ~ open s & req s = {}}, |
122 {request_act, open_act, close_act, |
121 {request_act, open_act, close_act, |
123 req_up, req_down, move_up, move_down})" |
122 req_up, req_down, move_up, move_down})" |
124 |
123 |
125 |
124 |
158 fixes |
157 fixes |
159 n :: int |
158 n :: int |
160 assumes |
159 assumes |
161 Min_le_n "Min <= n" |
160 Min_le_n "Min <= n" |
162 n_le_Max "n <= Max" |
161 n_le_Max "n <= Max" |
|
162 defines |
163 |
163 |
164 end |
164 end |