File tree Expand file tree Collapse file tree 2 files changed +0
-3
lines changed
Expand file tree Collapse file tree 2 files changed +0
-3
lines changed Original file line number Diff line number Diff line change @@ -377,8 +377,6 @@ proof. by apply/mset_eqP => x; rewrite !multE; smt(mult_ge0). qed.
377377lemma msetU0 (A : ' a mset) : A `|` mset0 = A.
378378proof. by apply/mset_eqP => x; rewrite !multE; smt(mult_ge0). qed.
379379
380- print maxrC.
381-
382380lemma msetUA (A B C : ' a mset) : A `|` (B `|` C) = A `|` B `|` C.
383381proof. by apply/mset_eqP => x; rewrite !multE maxrA. qed.
384382
Original file line number Diff line number Diff line change @@ -545,7 +545,6 @@ have eq_main_O1e_O1l: equiv[Game(A, O1e).main ~ Gr(O1l).main:
545545eager proc H (={glob Var}) => // ; 2: by sim.
546546 proc*; inline *; rcondf{2 } 6 ; [ by auto | by sp; if ; auto ].
547547proc.
548- print Game.
549548transitivity* {1 } {r <@ Game (A, O1e).main (d);}.
550549+ by inline *; rcondt{2 } 8 ; auto ; call(: ={Var.x }); 1 : sim; auto .
551550rewrite equiv[{1 } 1 eq_main_O1e_O1l].
You can’t perform that action at this time.
0 commit comments