equal
deleted
inserted
replaced
9 Follows = Union + |
9 Follows = Union + |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" |
13 Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set" |
14 (infixl 65) |
14 (infixl "Fols" 65) |
15 "f Follows g == Increasing g Int Increasing f Int |
15 "f Fols g == Increasing g Int Increasing f Int |
16 Always {s. f s <= g s} Int |
16 Always {s. f s <= g s} Int |
17 (INT k. {s. k <= g s} LeadsTo {s. k <= f s})" |
17 (INT k. {s. k <= g s} LeadsTo {s. k <= f s})" |
18 |
18 |
19 |
19 |
20 end |
20 end |