|
1
|
(* Generated by Frama-C WP *)
|
|
2
|
|
|
3
|
Goal typed_AltitudeControl_step_post.
|
|
4
|
Proof.
|
|
5
|
intros.
|
|
6
|
eapply Q_inv_inv_AltitudeControl.
|
|
7
|
Focus 4.
|
|
8
|
eassumption.
|
|
9
|
eassumption.
|
|
10
|
eassumption.
|
|
11
|
eassumption.
|
|
12
|
Qed.
|
|
13
|
|
|
14
|
Goal typed_lemma_inv_inv_AltitudeControl.
|
|
15
|
Proof.
|
|
16
|
intros.
|
|
17
|
generalize H2.
|
|
18
|
unfold P_inv_AltitudeControl.
|
|
19
|
(*Case 1/4 -> 2/4*)
|
|
20
|
(*nb var and hyps in case hyp: 0+1+0+0*)
|
|
21
|
(*nb goals in case goal : 3+0+1*)
|
|
22
|
intros h.
|
|
23
|
elim h;clear h.
|
|
24
|
(*nb: 1*)
|
|
25
|
intros ?.
|
|
26
|
(*choose case 2/4*)
|
|
27
|
right.
|
|
28
|
left.
|
|
29
|
repeat eapply ex_intro.
|
|
30
|
(*nb goals: 4(split one less)*)
|
|
31
|
split.
|
|
32
|
Focus 2.
|
|
33
|
split.
|
|
34
|
Focus 2.
|
|
35
|
split.
|
|
36
|
Focus 2.
|
|
37
|
eassumption.
|
|
38
|
eassumption.
|
|
39
|
eassumption.
|
|
40
|
eassumption.
|
|
41
|
(*Case 2/4 -> 3/4*)
|
|
42
|
(*nb var and hyps in case hyp: 8+3+0+1*)
|
|
43
|
(*nb goals in case goal : 5+0+2*)
|
|
44
|
intros h.
|
|
45
|
elim h;clear h.
|
|
46
|
(*nb: 12*)
|
|
47
|
intros [? [? [? [? [? [? [? [? [? [? [? ?]]]]]]]]]]].
|
|
48
|
(*choose case 3/4*)
|
|
49
|
right.
|
|
50
|
right.
|
|
51
|
left.
|
|
52
|
repeat eapply ex_intro.
|
|
53
|
(*nb goals: 7(split one less)*)
|
|
54
|
split.
|
|
55
|
Focus 2.
|
|
56
|
split.
|
|
57
|
Focus 2.
|
|
58
|
split.
|
|
59
|
Focus 2.
|
|
60
|
split.
|
|
61
|
Focus 2.
|
|
62
|
split.
|
|
63
|
Focus 2.
|
|
64
|
split.
|
|
65
|
Focus 2.
|
|
66
|
eassumption.
|
|
67
|
eassumption.
|
|
68
|
eassumption.
|
|
69
|
eassumption.
|
|
70
|
eassumption.
|
|
71
|
eassumption.
|
|
72
|
eassumption.
|
|
73
|
(*Case 3/4 -> 4/4*)
|
|
74
|
(*nb var and hyps in case hyp: 16+5+0+2*)
|
|
75
|
(*nb goals in case goal : 6+3+3*)
|
|
76
|
intros h.
|
|
77
|
elim h;clear h.
|
|
78
|
(*nb: 23*)
|
|
79
|
intros [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? ?]]]]]]]]]]]]]]]]]]]]]].
|
|
80
|
(*choose case 4/4*)
|
|
81
|
right.
|
|
82
|
right.
|
|
83
|
right.
|
|
84
|
repeat eapply ex_intro.
|
|
85
|
(*nb goals: 12(split one less)*)
|
|
86
|
split.
|
|
87
|
Focus 2.
|
|
88
|
split.
|
|
89
|
Focus 2.
|
|
90
|
split.
|
|
91
|
Focus 2.
|
|
92
|
split.
|
|
93
|
Focus 2.
|
|
94
|
split.
|
|
95
|
Focus 2.
|
|
96
|
split.
|
|
97
|
Focus 2.
|
|
98
|
split.
|
|
99
|
Focus 2.
|
|
100
|
split.
|
|
101
|
Focus 2.
|
|
102
|
split.
|
|
103
|
Focus 2.
|
|
104
|
split.
|
|
105
|
Focus 2.
|
|
106
|
split.
|
|
107
|
Focus 2.
|
|
108
|
eassumption.
|
|
109
|
eassumption.
|
|
110
|
eassumption.
|
|
111
|
eapply (Q_inv_init_3_AltitudeControl).
|
|
112
|
Focus 9.
|
|
113
|
eassumption.
|
|
114
|
Focus 8.
|
|
115
|
eassumption.
|
|
116
|
Focus 7.
|
|
117
|
eassumption.
|
|
118
|
eassumption.
|
|
119
|
eassumption.
|
|
120
|
eassumption.
|
|
121
|
eassumption.
|
|
122
|
eassumption.
|
|
123
|
eassumption.
|
|
124
|
eapply (Q_inv_init_2_AltitudeControl).
|
|
125
|
Focus 7.
|
|
126
|
eassumption.
|
|
127
|
Focus 6.
|
|
128
|
eassumption.
|
|
129
|
eassumption.
|
|
130
|
eassumption.
|
|
131
|
eassumption.
|
|
132
|
eassumption.
|
|
133
|
eassumption.
|
|
134
|
eapply (Q_inv_init_1_AltitudeControl).
|
|
135
|
Focus 5.
|
|
136
|
eassumption.
|
|
137
|
eassumption.
|
|
138
|
eassumption.
|
|
139
|
eassumption.
|
|
140
|
eassumption.
|
|
141
|
eassumption.
|
|
142
|
eassumption.
|
|
143
|
eassumption.
|
|
144
|
eassumption.
|
|
145
|
eassumption.
|
|
146
|
eassumption.
|
|
147
|
(*Case 4/4 -> 4/4*)
|
|
148
|
(*nb var and hyps in case hyp: 24+6+3+3*)
|
|
149
|
(*nb goals in case goal : 6+3+3*)
|
|
150
|
(*nb: 36*)
|
|
151
|
intros [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? [? ?]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]].
|
|
152
|
(*choose case 4/4*)
|
|
153
|
right.
|
|
154
|
right.
|
|
155
|
right.
|
|
156
|
repeat eapply ex_intro.
|
|
157
|
(*nb goals: 12(split one less)*)
|
|
158
|
split.
|
|
159
|
Focus 2.
|
|
160
|
split.
|
|
161
|
Focus 2.
|
|
162
|
split.
|
|
163
|
Focus 2.
|
|
164
|
split.
|
|
165
|
Focus 2.
|
|
166
|
split.
|
|
167
|
Focus 2.
|
|
168
|
split.
|
|
169
|
Focus 2.
|
|
170
|
split.
|
|
171
|
Focus 2.
|
|
172
|
split.
|
|
173
|
Focus 2.
|
|
174
|
split.
|
|
175
|
Focus 2.
|
|
176
|
split.
|
|
177
|
Focus 2.
|
|
178
|
split.
|
|
179
|
Focus 2.
|
|
180
|
eassumption.
|
|
181
|
eassumption.
|
|
182
|
eassumption.
|
|
183
|
eapply Q_inv_spec_AltitudeControl.
|
|
184
|
Focus 5.
|
|
185
|
eassumption.
|
|
186
|
eassumption.
|
|
187
|
eassumption.
|
|
188
|
eassumption.
|
|
189
|
eassumption.
|
|
190
|
eassumption.
|
|
191
|
eassumption.
|
|
192
|
eassumption.
|
|
193
|
eassumption.
|
|
194
|
eassumption.
|
|
195
|
eassumption.
|
|
196
|
eassumption.
|
|
197
|
eassumption.
|
|
198
|
Qed.
|
|
199
|
|
|
200
|
Goal typed_ref_AltitudeControl_step_post.
|
|
201
|
Proof.
|
|
202
|
intros.
|
|
203
|
eapply Q_inv_inv_AltitudeControl.
|
|
204
|
Focus 4.
|
|
205
|
eassumption.
|
|
206
|
eassumption.
|
|
207
|
eassumption.
|
|
208
|
eassumption.
|
|
209
|
Qed.
|
|
210
|
|
|
211
|
Goal typed_ref_AltitudeControl_step_stmt_post_20.
|
|
212
|
Hint AltitudeControl_step,default,property.
|
|
213
|
Proof.
|
|
214
|
Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;try why3 "CVC4" timelimit 10.
|
|
215
|
why3 "alt-ergo" timelimit 20.
|
|
216
|
Qed.
|
|
217
|
|
|
218
|
Goal typed_ref_lemma_missing.
|
|
219
|
Hint missing,property.
|
|
220
|
Proof.
|
|
221
|
admit.
|
|
222
|
Qed.
|
|
223
|
|
|
224
|
|