Skip to content

Commit e936226

Browse files
wadoonwadoon
committed
fix schiffl_lemma_2 to the new format
1 parent c0f5ede commit e936226

File tree

1 file changed

+57
-57
lines changed

1 file changed

+57
-57
lines changed

‎key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof‎

Lines changed: 57 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -55,58 +55,58 @@ rule "exLeft";
5555
macro "split-prop";
5656
// the following equations are useful in many case.
5757
rule seqNPermRange;
58-
instantiate var=iv with=`v_x_0` occ=1;
58+
instantiate var=iv with=(v_x_0) occ=1;
5959
rule impLeft;
6060
tryclose branch;
6161
rule andLeft;
6262
rule andLeft;
6363
// 1. triple of equations
64-
instantiate var=iv with=`v_y_0` occ=1;
64+
instantiate var=iv with=(v_y_0) occ=1;
6565
rule impLeft;
6666
tryclose branch;
6767
rule andLeft;
6868
rule andLeft;
6969
// 2. triple of equations
7070
rule seqNPermDefLeft;
71-
instantiate var=iv with=`v_x_0` occ=2;
71+
instantiate var=iv with=(v_x_0) occ=2;
7272
rule impLeft;
7373
tryclose branch;
7474
rule exLeft;
7575
rule andLeft;
7676
rule andLeft;
7777
// 3. triple of equations
78-
instantiate hide var=iv with=`v_y_0` occ=2;
78+
instantiate hide var=iv with=(v_y_0) occ=2;
7979
rule impLeft;
8080
tryclose branch;
8181
rule exLeft;
8282
rule andLeft;
8383
rule andLeft;
8484
// 4. triple of equations
85-
instantiate var=iv with=`jv_0` occ=1;
85+
instantiate var=iv with=(jv_0) occ=1;
8686
rule impLeft;
8787
tryclose branch;
8888
rule andLeft;
8989
rule andLeft;
90-
rule castAdd formula=`s_0[jv_0] = v_x_0` occ=0;
90+
rule castAdd formula=(s_0[jv_0] = v_x_0) occ=0;
9191
// 5. set of equations
92-
instantiate hide var=iv with=`jv_1` occ=1;
92+
instantiate hide var=iv with=(jv_1) occ=1;
9393
rule impLeft;
9494
tryclose branch;
9595
rule andLeft;
9696
rule andLeft;
97-
rule castAdd formula=`s_0[jv_1] = v_y_0` occ=0;
97+
rule castAdd formula=(s_0[jv_1] = v_y_0) occ=0;
9898
// 6. set of equations
99-
instantiate var=iv with=`v_x_0`;
99+
instantiate var=iv with=(v_x_0);
100100
rule impLeft;
101101
tryclose branch;
102102
// 7. equation
103-
instantiate var=iv with=`v_y_0`;
103+
instantiate var=iv with=(v_y_0);
104104
rule impLeft;
105105
tryclose branch;
106106
// 8. equation
107-
cut `v_x_0 = v_y_0`;
107+
cut (v_x_0 = v_y_0);
108108
// This corresponds to case A in the Notes.
109-
instantiate hide var="v_r" with=`seqSwap(s_0,v_x_0,jv_0)`;
109+
instantiate hide var="v_r" with=(seqSwap(s_0,v_x_0,jv_0));
110110
// in the following r refers to this instantiation
111111
rule andRight;
112112
rule andRight;
@@ -116,16 +116,16 @@ rule lenOfSwap;
116116
tryclose branch;
117117
// established: r is of correct length
118118
rule seqNPermSwapNPerm;
119-
instantiate hide var="iv" with=`v_x_0` occ=1;
120-
instantiate hide var="jv" with=`jv_0`;
119+
instantiate hide var="iv" with=(v_x_0) occ=1;
120+
instantiate hide var="jv" with=(jv_0);
121121
rule impLeft;
122122
tryclose branch;
123123
tryclose branch;
124124
// established: r is permutation
125125
rule allRight;
126126
rule impRight;
127127
rule andLeft;
128-
instantiate var="iv" with=`v_iv_0`;
128+
instantiate var="iv" with=(v_iv_0);
129129
rule impLeft;
130130
tryclose branch;
131131
rule getOfSwap;
@@ -164,17 +164,17 @@ tryclose branch;
164164
tryclose branch;
165165
// established: r fixes v_y_0
166166
// from now on v_x_0 != v_y_0
167-
cut `(int)s_0[v_x_0]=(int)s_0[v_y_0]`;
167+
cut ((int)s_0[v_x_0]=(int)s_0[v_y_0]);
168168
rule seqNPermInjective;
169-
instantiate hide var=iv with=`v_x_0`;
170-
instantiate hide var=jv with=`v_y_0`;
169+
instantiate hide var=iv with=(v_x_0);
170+
instantiate hide var=jv with=(v_y_0);
171171
rule impLeft;
172172
tryclose branch;
173173
tryclose branch;
174174
// from now on s_0[v_x_0] != v_x_0
175-
cut `(int)s_0[v_x_0] = v_x_0`;
175+
cut ((int)s_0[v_x_0] = v_x_0);
176176
// This corresponds to case B1 & B2 in the Notes.
177-
instantiate hide var=v_r with=`seqSwap(s_0,v_y_0,jv_1)`;
177+
instantiate hide var=v_r with=(seqSwap(s_0,v_y_0,jv_1));
178178
// in the following r1 refers to this instantion
179179
rule andRight;
180180
rule andRight;
@@ -183,14 +183,14 @@ rule andRight;
183183
tryclose branch;
184184
// established: r1 is of the correct length
185185
rule seqNPermSwapNPerm;
186-
instantiate hide var=iv with=`v_y_0`;
187-
instantiate hide var=jv with=`jv_1`;
186+
instantiate hide var=iv with=(v_y_0);
187+
instantiate hide var=jv with=(jv_1);
188188
tryclose branch;
189189
// established: r1 is permutation
190190
rule allRight;
191191
rule impRight;
192192
rule andLeft;
193-
instantiate var=iv with=`v_iv_0`;
193+
instantiate var=iv with=(v_iv_0);
194194
rule impLeft;
195195
tryclose branch;
196196
rule getOfSwap;
@@ -203,7 +203,7 @@ rule ifthenelse_split occ=0;
203203
tryclose branch;
204204
rule ifthenelse_split occ=0;
205205
tryclose branch;
206-
instantiate var=iv with=`v_y_0`;
206+
instantiate var=iv with=(v_y_0);
207207
rule impLeft;
208208
tryclose branch;
209209
tryclose branch;
@@ -219,9 +219,9 @@ tryclose branch;
219219
tryclose branch;
220220
// established: r1 fixes v_y_0
221221
// from now on v_x_0 != v_y_0 and s_0[v_x_0]!= v_x_0
222-
cut `(int)s_0[v_y_0] = v_y_0`;
222+
cut ((int)s_0[v_y_0] = v_y_0);
223223
// This corresponds to case B3 in the Notes.
224-
instantiate hide var=v_r with=`seqSwap(s_0,v_x_0,jv_0)`;
224+
instantiate hide var=v_r with=(seqSwap(s_0,v_x_0,jv_0));
225225
// in the following r2 refers to this instantion
226226
rule andRight;
227227
rule andRight;
@@ -230,16 +230,16 @@ rule andRight;
230230
tryclose branch;
231231
// established: r2 is of the correct length
232232
rule seqNPermSwapNPerm;
233-
instantiate hide var=iv with=`v_x_0`;
234-
instantiate hide var=jv with=`jv_0`;
233+
instantiate hide var=iv with=(v_x_0);
234+
instantiate hide var=jv with=(jv_0);
235235
rule impLeft;
236236
tryclose branch;
237237
tryclose branch;
238238
// established: r2 is permutation
239239
rule allRight;
240240
rule impRight;
241241
rule andLeft;
242-
instantiate var=iv with=`v_iv_0`;
242+
instantiate var=iv with=(v_iv_0);
243243
rule impLeft;
244244
tryclose branch;
245245
rule getOfSwap;
@@ -268,9 +268,9 @@ tryclose branch;
268268
tryclose branch;
269269
// established: r2 fixes v_y_0
270270
// from now on v_x_0 != v_y_0 and s_0[v_x_0]!= v_x_0 and s_0[v_y_0]!= v_y_0
271-
cut `(int)s_0[v_x_0]=v_y_0`;
271+
cut ((int)s_0[v_x_0]=v_y_0);
272272
// This corresponds to case B4i & B4iii in the Notes.
273-
instantiate hide var=v_r with=`seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)`;
273+
instantiate hide var=v_r with=(seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0));
274274
// in the following r3 refers to this instantion
275275
rule andRight;
276276
rule andRight;
@@ -279,13 +279,13 @@ rule andRight;
279279
tryclose branch;
280280
// established: r3 is of the correct length
281281
rule seqNPermSwapNPerm;
282-
instantiate hide var=iv with=`jv_0`;
283-
instantiate hide var=jv with=`v_x_0`;
282+
instantiate hide var=iv with=(jv_0);
283+
instantiate hide var=jv with=(v_x_0);
284284
rule impLeft;
285285
tryclose branch;
286-
rule seqNPermSwapNPerm formula=`seqNPerm(seqSwap(s_0, jv_0, v_x_0))`;
287-
instantiate hide var=iv with=`jv_0`;
288-
instantiate hide var=jv with=`v_y_0`;
286+
rule seqNPermSwapNPerm formula=(seqNPerm(seqSwap(s_0, jv_0, v_x_0)));
287+
instantiate hide var=iv with=(jv_0);
288+
instantiate hide var=jv with=(v_y_0);
289289
rule impLeft;
290290
tryclose branch;
291291
tryclose branch;
@@ -295,7 +295,7 @@ rule impRight;
295295
rule andLeft;
296296
// start: providing equation for latter use
297297
// in many case distinctions
298-
instantiate var=iv with=`v_iv_0`;
298+
instantiate var=iv with=(v_iv_0);
299299
rule impLeft;
300300
tryclose branch;
301301
// end: providing equation for latter use
@@ -370,19 +370,19 @@ tryclose branch;
370370
// established: r3 fixes v_y_0
371371
// from now on v_x_0 != v_y_0 and s_0[v_x_0]!= v_x_0 and
372372
// s_0[v_y_0]!= v_y_0 and s_0[v_x_0]!= v_y_0
373-
cut `int::seqGet(s_0, v_y_0)=v_x_0`;
373+
cut (int::seqGet(s_0, v_y_0)=v_x_0);
374374
// This corresponds to case B4ii in the Notes.
375375
// in the following r4 refers to this instantion
376376
tryclose branch;
377377
// established: r4 is of the correct length
378378
rule seqNPermSwapNPerm;
379-
instantiate hide var=iv with=`jv_1`;
380-
instantiate hide var=jv with=`v_y_0`;
379+
instantiate hide var=iv with=(jv_1);
380+
instantiate hide var=jv with=(v_y_0);
381381
rule impLeft;
382382
tryclose branch;
383-
rule seqNPermSwapNPerm formula=`seqNPerm(seqSwap(s_0,jv_1,v_y_0))`;
384-
instantiate hide var=iv with=`jv_1`;
385-
instantiate hide var=jv with=`v_x_0`;
383+
rule seqNPermSwapNPerm formula=(seqNPerm(seqSwap(s_0,jv_1,v_y_0)));
384+
instantiate hide var=iv with=(jv_1);
385+
instantiate hide var=jv with=(v_x_0);
386386
rule impLeft;
387387
tryclose branch;
388388
tryclose branch;
@@ -394,24 +394,24 @@ tryclose branch;
394394
// in the following r5 refers to this instantion
395395
tryclose branch;
396396
// established: r5 is of the correct length
397-
rule seqNPermSwapNPerm formula=`seqNPerm(s_0)`;
398-
instantiate hide var=iv with=`v_x_0`;
399-
instantiate hide var=jv with=`jv_0`;
397+
rule seqNPermSwapNPerm formula=(seqNPerm(s_0));
398+
instantiate hide var=iv with=(v_x_0);
399+
instantiate hide var=jv with=(jv_0);
400400
rule impLeft;
401401
tryclose branch;
402-
rule seqNPermSwapNPerm formula=`seqNPerm(seqSwap(s_0,v_x_0,jv_0))`;
403-
instantiate hide var=iv with=`v_y_0`;
404-
instantiate hide var=jv with=`jv_1`;
405-
instantiate hide var=v_r with=`seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)`;
402+
rule seqNPermSwapNPerm formula=(seqNPerm(seqSwap(s_0,v_x_0,jv_0)));
403+
instantiate hide var=iv with=(v_y_0);
404+
instantiate hide var=jv with=(jv_1);
405+
instantiate hide var=v_r with=(seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1));
406406
tryclose branch;
407-
rule seqNPermSwapNPerm formula=`seqNPerm(s_0)`;
408-
instantiate hide var=iv with=`v_x_0`;
409-
instantiate hide var=jv with=`jv_0`;
407+
rule seqNPermSwapNPerm formula=(seqNPerm(s_0));
408+
instantiate hide var=iv with=(v_x_0);
409+
instantiate hide var=jv with=(jv_0);
410410
rule impLeft;
411411
tryclose branch;
412-
rule seqNPermSwapNPerm formula=`seqNPerm(seqSwap(s_0,v_x_0,jv_0))`;
413-
instantiate hide var=iv with=`v_y_0`;
414-
instantiate hide var=jv with=`jv_1`;
415-
instantiate hide var=v_r with=`seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)`;
412+
rule seqNPermSwapNPerm formula=(seqNPerm(seqSwap(s_0,v_x_0,jv_0)));
413+
instantiate hide var=iv with=(v_y_0);
414+
instantiate hide var=jv with=(jv_1);
415+
instantiate hide var=v_r with=(seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1));
416416
tryclose branch;
417417
}

0 commit comments

Comments
 (0)