We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 82c4133 commit a28e4c5Copy full SHA for a28e4c5
1 file changed
proofs/OpenPRE_From_TCR_DSPR_THF.eca
@@ -1276,10 +1276,9 @@ seq 1 :
1276
/\ (size O_SMDTOpenPRE_Default.ts <= _jj)
1277
/\ _j{hr} = _jj); 1: by auto;smt(size_ge0 mem_rcons nth_rcons size_rcons).
1278
by wp;call(:true);auto => />; smt(ge0_t size_ge0).
1279
- if;sp 1;seq 1 : #pre;1: by auto.
1280
- + by auto => />;smt(nth_rcons size_rcons).
+ if; 1:(sp 1;seq 1 : #pre;1: by auto).
+ + by auto => />;smt(nth_rcons size_rcons).
1281
by auto => />;smt(nth_rcons size_rcons).
1282
-by auto => />;smt(nth_rcons size_rcons).
1283
1284
+ call (_ : (glob A) = (glob A){m} /\ arg.`1 = _ii /\ arg.`2 = _jj ==>
1285
res.`3 = _jj /\ O_SMDTOpenPRE_Default_early_fail.r
0 commit comments