diff --git a/.obsidian/app.json b/.obsidian/app.json
index 6abe4c1..e69de29 100644
--- a/.obsidian/app.json
+++ b/.obsidian/app.json
@@ -1,3 +0,0 @@
-{
-  "alwaysUpdateLinks": true
-}
\ No newline at end of file
diff --git a/4a1s/MFES/PL - Aula 9.md b/4a1s/MFES/PL - Aula 9.md
index 7c9ff54..6e5501a 100644
--- a/4a1s/MFES/PL - Aula 9.md	
+++ b/4a1s/MFES/PL - Aula 9.md	
@@ -165,15 +165,14 @@ module SelectionSort
     ensures { sorted a }
     ensures { permut_all (old a) a }
   = for i = 0 to length a - 1 do
-      invariant { ... }
+      invariant { sorted_sub a 0 i }
+      invariant { forall k1 k2:int. 0<= k1<i<=k2<length a -> a[k1]<=a[k2]}
+      invariant { permut_all (old a) a }
       let min = select a i
       in if min <> i then swap a min i
     done
 
 
-
-
-
   let selection_sort_2 (a: array int) =
     ensures { sorted a }
     ensures { permut_all (old a) a }
@@ -181,6 +180,11 @@ module SelectionSort
 
 
 end      
+```
 
 
-```
\ No newline at end of file
+
+https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpBJ1Theyselection%2F2sortyalgorithm%2F3sorts0an3arrayBH0byysuccessively%2F5placing0in2each6position1theBH%2Fi%2BA%2Bc2next5minimum%2Fi%2BA%2BdB5element7r0as5follows7vNH72040o020s010s030s060sz0s08074HkpplslslslskskkHkkplskskskskskkHkkpkskskskskskkHkkpkskskskskskkHkkpkskskslskskkHkkpkskskskskskkHkkpkskskskskskkNEz17t6Completea6contract0of6function2swapj5writingBK6adequate1preA7s1and2postArAyconditions%2FfH4Recall2that7h4lengthzar3gives1youZyallocated%2FnHZuHliEz2s3WriteqV1forU4selectnBKn2also1one0or2more2loopyinvariants%2FX3allowHY0to3proveWycorrectness%2FXrcdBH2NotejYg5variant0is1not6required7r3sinceBH7hSs3loops1are5boundedeBEz3sPQQQcQZQQQQKSQQyselection%2Bsort%2B1%2FeBH1You1may2needk4modifykulkuluK3orderBHQnZyinvariant%2Fmei0be4provedcBEz4s5Finally7r3writehuEyselection%2Bsort%2B2%2Fp3which2doesKuo1usemukWh0It2will2haveza4nestedU7wBHbuwR2bothupubuxcuxHu5rTbBN7JoCCBNNN4moduleySelectionSort%2FNFV1intoA1IntHq1refqA1RefHquhqA3ArrayHqqqAyIntArraySorted%2FHqqqyArrayPermut%2FHqqq5ArrayEqNNNH1letuX7nO7vme7ooziopppzjpppBJ6requires77z07RykA7xufg7FlnnhAnnn79H5ensuresCje1oldo7I2g747ypA72gpdkknknnlpAlkphHhCh4forallzkXAXSBYAYAoYAYe7MzpA7RzAdqqAqAaqXXmXlZXpAXk7Y9HXCXypermut%2Ball%2FhhlSsUFiPzvrpAgeeuzJpppp7Rsppc7YwHqqqookNNNFuA5returnsvN3indexvMjCuLrBKp5segmentrp5between5indexesdvIvdoB7sAz17tBFvLGUu9Pm7vvVvY7oofopprrJvV77z0vXmB7xbhA79HvbClnm4resultBllllHlClvWzkfAfYBfAgAoAhAhhvXs72e74lpplvYF7yUvN1minqXvZLvEzjpp7qz1u0aeB7sBp0doJuyQkZeBVfBOHmmPXPAPPBhhoBiiQcSeRlpplpdH0ifookojppkp2thenrvXmF2done7wFpNNKMBvouy7niYviX7oBJvjT4sortedmYHppvTjvTnlsmF7yvlQrz0vlvlm7sz1vlLvldysorted%2Bsub%2FnkigHnnvl0k10k2UAV7tjAvmnA7xAhAqAlAqAbfvls72l7YRyAqqmviHccQQQlQsXHvpvoPvfoYHvivinBvRBpvhvPmopFvhNNNNNFiu1dn7vvhvobcJviXvhlYHppWiWnksmF7NNtNNN1endCCCNN
+
+
+https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpBJ3Writeyappropriate%2Fydefinitions%2F1andyspecifications%2F1forHyfunctions%2F3splitp3merge7r2used0by1thep2sortBHyalgorithm%2F5defined3below0inn4module7tBHH2Note2thatpyverification%2F0ofymergesort%2F4relies2onlyBH0onnV7Hhycontracts%2F7Bokoyauxiliary%2FBHSUT1noti3their2codeZ0As2suchl0it0is5crucialH0to5includeQ2them3every4aspect6requireduEXHOyconditions%2FUq5sortinguJHg0beysuccessfully%2Fydischarged%2FWHHuM2alsouM6although2Why3V5capableeyautomatically%2FBH5provingcytermination%2FpuU2with4simpleyrecursive%2FH6patterns7re2doesuV3applyUguM6functionVBH0We2thusububm6contracts5variant7h4lengthzl7BrBH3whichO3valid3sincekdpyrecursively%2F4calledBHuU3listsT1are5shorter2thaneVBN7JoCCNNNNuLyMergeSort%2FNF1use1intoA1IntHq2listqA2ListHqqqA4LengthHqqqA4PermutHqqq4AppendHqqqySortedInt%2FNNNH1let1recUuE7nbB7vAkd7oqopp7rrroJ5ensures77hm0l1l0l2m7y4resultu64permutekkA7KqAkk79HffAfllfAllfffu8fA7xAz27c8hooA7TyAo7FlBLpfAlArgprrBqBrp7I9MBg3matchCjuuBMH781Nil7MzerZsZHo2ConszxpmmklplHlllmrzyztnjUndiandvVkLUlhgjjqgiiBMB1endNNNHgvTvTuGhilB7vAvSvSiqBqqJ6requires774sortedlvYrk79HvUCnBpvUApBHppAvSpfkAvSAkvVFQvVoTovVJvVqz%2BvVoH78qpoomHohOzxp7GIrppzyi7Gok0ifkA7RyAnL2thenlpkvbhA7mBh7oH2elseljlllmfMBvXNNHHvXvXvXu0kzl7vvWvWcJvZ77vYvZ79BHppvYjoBoBHu4ovSopF7yJvYqvYH78vYvZsHrPzxqpqqqHpz%2BoCBTWP7rAOWevSeMMvSvbkPjlqqkqMDvcNNNNFypredicate%2Fyis%2Ba%2Bsorting%2Balgorithm%2FnzfA7vvevearrkcBJ4forall0almnn7tBvgoiirj7O3veooooNF2goaleBhsaNNNNb
\ No newline at end of file