| changeset 49892 | 09956f7a00af |
| parent 49579 | 1c73b107d20d |
| child 50986 | c54ea7f5418f |
| 49891:a6563caedf7a | 49892:09956f7a00af |
|---|---|
702 |
702 |
703 because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2, |
703 because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2, |
704 which is again not a pfp: not f 2 = 3 <= 2 |
704 which is again not a pfp: not f 2 = 3 <= 2 |
705 Another widening step yields 2 widen f 2 = 2 widen 3 = 3 |
705 Another widening step yields 2 widen f 2 = 2 widen 3 = 3 |
706 *) |
706 *) |
707 |
707 oops |
708 end |
708 |
709 end |