Project

General

Profile

Download (3.49 KB) Statistics
| Branch: | Tag: | Revision:
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.
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;why3 "CVC4" timelimit 10. *)
215
Qed.
216

    
217
Goal typed_ref_VariableRateLimit_step_stmt_post_4.
218
Hint VariableRateLimit_step,default,property.
219
Proof.
220
(* Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10. *)
221
Qed.
222

    
223

    
(2-2/4)