1
00:00:02,420 --> 00:00:03,380
下面这个，我们来看
2
00:00:03,390 --> 00:00:09,940
X→select（Y），用Y这个条件来筛选
3
00:00:09,950 --> 00:00:11,340
之后得到的集合
4
00:00:12,400 --> 00:00:14,390
forAll这个意思是什么
5
00:00:14,400 --> 00:00:17,950
集合里面所有的元素都符合这个条件
6
00:00:18,540 --> 00:00:22,470
这不是筛选，是符合这个条件的意思
7
00:00:24,060 --> 00:00:25,820
就是Y筛选过之后
8
00:00:26,170 --> 00:00:28,990
得到的所有的元素都符合这个条件
9
00:00:29,850 --> 00:00:31,560
实际上就等价于什么
10
00:00:32,840 --> 00:00:34,960
对X里面的所有元素
11
00:00:36,040 --> 00:00:40,700
如果Y，那么就符合Z
12
00:00:40,710 --> 00:00:43,140
如果Y，那么Z，实际上就是一个蕴含的关系
13
00:00:48,530 --> 00:00:51,840
这些我们之前讲过的，后面这两个没讲
14
00:00:51,930 --> 00:00:54,670
前面讲过的，这些表达式我们都可以
15
00:00:55,850 --> 00:00:57,730
这些公式我们都可以用来
16
00:00:59,050 --> 00:01:04,590
作为我们简化或者推导不变式
17
00:01:05,910 --> 00:01:12,090
或者其他的表达式的一个工具
18
00:01:13,430 --> 00:01:17,000
比如说，还是这个员工部门
19
00:01:17,410 --> 00:01:20,050
员工，部门
20
00:01:21,980 --> 00:01:24,650
员工有姓名、年龄、薪水
21
00:01:24,940 --> 00:01:27,690
部门有名称，有最低薪水、高档薪水
22
00:01:28,770 --> 00:01:29,640
假设有这样一个
23
00:01:29,650 --> 00:01:32,260
如果员工年龄未达35岁的话
24
00:01:32,580 --> 00:01:35,550
那么薪水不得超过部门高档薪水
25
00:01:39,500 --> 00:01:40,990
如果我们针对部门做不变式
26
00:01:41,000 --> 00:01:45,600
可能一开始
27
00:01:45,610 --> 00:01:48,770
会得到这样一个
28
00:01:49,040 --> 00:01:51,120
员工，然后给一个条件
29
00:01:52,020 --> 00:01:55,710
小于35岁的员工的集合里面
30
00:01:59,000 --> 00:02:01,870
存在薪水大于高档薪水的
31
00:02:01,880 --> 00:02:03,910
这样一个人是不行的
32
00:02:04,460 --> 00:02:07,830
就是说，不允许集合里面
33
00:02:08,280 --> 00:02:11,260
存在这样的人
34
00:02:12,730 --> 00:02:16,590
存在符合这个条件的元素
35
00:02:18,260 --> 00:02:19,970
这个看起来就比较复杂了
36
00:02:20,610 --> 00:02:25,320
我们可以用前面的公式先把存在去除掉
37
00:02:25,330 --> 00:02:26,400
38
00:02:27,600 --> 00:02:29,280
这个存在我们就可以说
39
00:02:31,360 --> 00:02:32,950
对所有人来说都不符合这个
40
00:02:33,820 --> 00:02:34,380
41
00:02:34,390 --> 00:02:37,630
对所有来说不符合这个
42
00:02:38,830 --> 00:02:40,110
我们就可以这样
43
00:02:41,310 --> 00:02:43,020
前面不变，这个就变成什么
44
00:02:43,030 --> 00:02:48,800
就变成员工
45
00:02:49,420 --> 00:02:53,010
然后所有的员工都符合这个条件
46
00:02:55,830 --> 00:02:58,390
员工的薪水
47
00:02:58,910 --> 00:03:00,230
不得大于高档薪水
48
00:03:09,510 --> 00:03:11,780
你看，select之后就符合这个条件
49
00:03:12,170 --> 00:03:13,560
我们可以就把它变成
50
00:03:13,570 --> 00:03:14,950
把这个挪过来
51
00:03:15,080 --> 00:03:16,190
针对所有员工
52
00:03:16,930 --> 00:03:18,130
这就是推导关系了
53
00:03:18,140 --> 00:03:19,690
只要你小于35岁
54
00:03:20,300 --> 00:03:23,960
那么这个可以推导到这个
55
00:03:26,580 --> 00:03:30,000
而这个蕴含关系的话
56
00:03:30,010 --> 00:03:34,260
我们用前面那个，P蕴含Q就等于什么
57
00:03:35,210 --> 00:03:38,900
非P或Q
58
00:03:38,910 --> 00:03:40,500
那就把它变成
59
00:03:40,510 --> 00:03:45,720
变成非P或Q，然后再用什么
60
00:03:45,730 --> 00:03:51,510
再用德摩根把它解开
61
00:03:51,770 --> 00:03:52,480
把它解开
62
00:03:53,550 --> 00:03:58,000
把这个not移除掉
63
00:03:58,010 --> 00:04:00,610
变成：所有的员工都符合这个条件
64
00:04:00,700 --> 00:04:02,890
要么年龄大于35岁
65
00:04:04,060 --> 00:04:05,970
要么薪水小于高档薪水
66
00:04:06,100 --> 00:04:07,450
这个就简单多了
