remove remaining axioms in one part of ih precond

Author: stefan-aws

audit.log

@@ -48,8 +48,6 @@ src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declarati
 src/ProbabilisticProgramming/RandomSource.dfy(67,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
 src/Util/FisherYates/Correctness.dfy(117,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
 src/Util/FisherYates/Correctness.dfy(126,12): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(185,16): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(188,16): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(217,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(242,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
-src/Util/FisherYates/Correctness.dfy(245,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
+src/Util/FisherYates/Correctness.dfy(221,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
+src/Util/FisherYates/Correctness.dfy(246,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 
+src/Util/FisherYates/Correctness.dfy(249,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body. 

src/Util/FisherYates/Correctness.dfy

@@ -182,11 +182,15 @@ module FisherYates.Correctness {
             assert |xs| == |ys|;
             calc {
               multiset(ys[i+1..]);
-              { assume {:axiom} false; }
-              // { assert ys[i+1..] == ys[i+1..j] + [ys[j]] + ys[j+1..]; }
+              { assert i+1 <= j; assert ys[i+1..] == ys[i+1..j] + ys[j..]; }
+              multiset(ys[i+1..j] + ys[j..]);
+              { assert ys[j..] == [ys[j]] + ys[j+1..]; }
               multiset(ys[i+1..j] + [ys[j]] + ys[j+1..]);
-              { assume {:axiom} false; }
-              //{ assert ys[i+1..j] == xs[i+1..j]; assert ys[j] == xs[i]; assert ys[j+1..] == xs[j+1..]; }
+              { assert ys[i+1..j] == xs[i+1..j];}
+              multiset(xs[i+1..j] + [ys[j]] + ys[j+1..]);
+              { assert ys[j] == xs[i]; }
+              multiset(xs[i+1..j] + [xs[i]] + ys[j+1..]);
+              { assert ys[j+1..] == xs[j+1..]; }
               multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]);
               { assert multiset([xs[j]]) - multiset([xs[j]]) == multiset{}; }
               multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]) + multiset([xs[j]]) - multiset([xs[j]]);