We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 32fac0f commit 9d63990Copy full SHA for 9d63990
1 file changed
key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof
@@ -385,14 +385,14 @@ instantiate hide var=iv with=(jv_1);
385
instantiate hide var=jv with=(v_x_0);
386
rule impLeft;
387
tryclose branch;
388
-tryclose branch;
+// tryclose branch;
389
// established: r4 is permutation
390
// established: r4 fixes v_y_0
391
// from now on v_x_0 != v_y_0 and s_0[v_x_0]!= v_x_0 and
392
// s_0[v_y_0]!= v_y_0 and s_0[v_x_0]!= v_y_0 and s_0[v_y_0]!=v_x_0;
393
// this corresponds to case B4iv in the Notes
394
// in the following r5 refers to this instantion
395
+//tryclose branch;
396
// established: r5 is of the correct length
397
rule seqNPermSwapNPerm formula=(seqNPerm(s_0));
398
instantiate hide var=iv with=(v_x_0);
0 commit comments