Return to non-incremental validation in numerical abduction. Map-base…

…d numerical substitutions and normal form inequalities.

examples/avl_tree.gadti.target

@@ -21,18 +21,18 @@ external val compare : ∀a. a → a → LinOrder
 val height : ∀n, a. Avl (a, n) → Num n
 
 val create :
-   ∀k, n, a[0 ≤ n ∧ n ≤ k + 2 ∧ 0 ≤ k ∧ k ≤ n + 2].
+   ∀k, n, a[k ≤ n + 2 ∧ 0 ≤ k ∧ n ≤ k + 2 ∧ 0 ≤ n].
    Avl (a, k) → a → Avl (a, n) → ∃i[i=max (k + 1, n + 1)].Avl (a, i)
 
 val singleton : ∀a. a → Avl (a, 1)
 
 val rotr :
-   ∀k, n, a[0 ≤ n ∧ n + 2 ≤ k ∧ k ≤ n + 3].
+   ∀k, n, a[k ≤ n + 3 ∧ n + 2 ≤ k ∧ 0 ≤ n].
    Avl (a, k) → a → Avl (a, n) → ∃n[k ≤ n ∧
      n ≤ k + 1].Avl (a, n)
 
 val rotl :
-   ∀k, n, a[n ≤ k + 3 ∧ 0 ≤ k ∧ k + 2 ≤ n].
+   ∀k, n, a[k + 2 ≤ n ∧ 0 ≤ k ∧ n ≤ k + 3].
    Avl (a, k) → a → Avl (a, n) → ∃k[k ≤ n + 1 ∧
      n ≤ k].Avl (a, k)
 
@@ -46,13 +46,13 @@ val min_binding : ∀n, a[1 ≤ n]. Avl (a, n) → a
 
 val remove_min_binding :
    ∀n, a[1 ≤ n].
-   Avl (a, n) → ∃k[n ≤ k + 1 ∧ k + 2 ≤ 2 n ∧ k ≤ n].Avl (a, k)
+   Avl (a, n) → ∃k[k + 2 ≤ 2 n ∧ k ≤ n ∧ n ≤ k + 1].Avl (a, k)
 
 val merge :
-   ∀k, n, a[n ≤ k + 2 ∧ k ≤ n + 2].
+   ∀k, n, a[k ≤ n + 2 ∧ n ≤ k + 2].
    (Avl (a, n), Avl (a, k)) → ∃i[n ≤ i ∧ k ≤ i ∧ i ≤ n + k ∧
      i≤max (k + 1, n + 1)].Avl (a, i)
 
 val remove :
    ∀n, a.
-   a → Avl (a, n) → ∃k[n ≤ k + 1 ∧ 0 ≤ k ∧ k ≤ n].Avl (a, k)
+   a → Avl (a, n) → ∃k[n ≤ k + 1 ∧ k ≤ n ∧ 0 ≤ k].Avl (a, k)

examples/binary_upper_bound.gadti.target

@@ -8,5 +8,5 @@ datacons POne : ∀n[0 ≤ n].Binary n ⟶ Binary (2 n + 1)
 
 val ub :
    ∀k, n.
-   Binary k → Binary n → ∃i[k ≤ i ∧ n ≤ i ∧
-     i ≤ n + k].Binary i
+   Binary k → Binary n → ∃i[i ≤ n + k ∧ n ≤ i ∧
+     k ≤ i].Binary i

examples/filter.gadti.target

@@ -6,4 +6,4 @@ datacons LCons : ∀n, a[0 ≤ n].a * List (a, n) ⟶ List (a, n + 1)
 
 val filter :
    ∀n, a.
-   (a → Bool) → List (a, n) → ∃k[0 ≤ k ∧ k ≤ n].List (a, k)
+   (a → Bool) → List (a, n) → ∃k[k ≤ n ∧ 0 ≤ k].List (a, k)

examples/filter_map.gadti.target

@@ -6,5 +6,5 @@ datacons LCons : ∀n, a[0 ≤ n].a * List (a, n) ⟶ List (a, n + 1)
 
 val filter :
    ∀n, a, b.
-   (a → Bool) → (a → b) → List (a, n) → ∃k[0 ≤ k ∧
-     k ≤ n].List (b, k)
+   (a → Bool) → (a → b) → List (a, n) → ∃k[k ≤ n ∧
+     0 ≤ k].List (b, k)

examples/liquid_bcopy.gadti.target

@@ -17,7 +17,7 @@ external val prod : Int → Int → Int
 external val int0 : Int
 
 val bcopy_aux :
-   ∀i, j, k, n, a[0 ≤ n ∧ k ≤ i ∧ k ≤ j].
+   ∀i, j, k, n, a[k ≤ j ∧ k ≤ i ∧ 0 ≤ n].
    Array (a, j) → Array (a, i) → (Num n, Num k) → ()
 
 val bcopy : ∀k, n, a[k ≤ n]. Array (a, k) → Array (a, n) → ()

examples/liquid_bcopy_simpler.gadti.target

@@ -17,7 +17,7 @@ external val prod : Int → Int → Int
 external val int0 : Int
 
 val bcopy_aux :
-   ∀i, j, k, n, a[0 ≤ n ∧ k ≤ i ∧ k ≤ j].
+   ∀i, j, k, n, a[k ≤ j ∧ k ≤ i ∧ 0 ≤ n].
    Array (a, j) → Array (a, i) → (Num n, Num k) → ()
 
 val bcopy : ∀k, n, a[k ≤ n]. Array (a, k) → Array (a, n) → ()

examples/liquid_bsearch.gadti.target

@@ -31,7 +31,7 @@ datacons NotFound : ∀a. Answer a
 datacons Found : ∀a.a ⟶ Answer a
 
 val look :
-   ∀i, k, n, a[0 ≤ k ∧ n + 1 ≤ i].
+   ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k].
    a → Array (a, i) → Num k → Num n → Answer a
 
 val bsearch : ∀n, a[0 ≤ n]. a → Array (a, n) → Answer a

examples/liquid_bsearch2.gadti.target

@@ -25,10 +25,10 @@ external val equal : ∀a. a → a → Bool
 external val div2 : ∀n. Num (2 n) → Num n
 
 val look :
-   ∀i, k, n, a[0 ≤ n + 1 ∧ 0 ≤ k ∧ n + 1 ≤ i].
-   a → Array (a, i) → Num k → Num n → ∃k[0 ≤ k + 1 ∧
-     k ≤ n].Num k
+   ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n + 1].
+   a → Array (a, i) → Num k → Num n → ∃k[k ≤ n ∧
+     0 ≤ k + 1].Num k
 
 val bsearch :
    ∀n, a[0 ≤ n + 1].
-   a → Array (a, n + 1) → ∃k[0 ≤ k + 1 ∧ k ≤ n].Num k
+   a → Array (a, n + 1) → ∃k[k ≤ n ∧ 0 ≤ k + 1].Num k

examples/liquid_bsearch2_harder1.gadti.target

@@ -25,10 +25,10 @@ external val equal : ∀a. a → a → Bool
 external val div2 : ∀n. Num (2 n) → Num n
 
 val look :
-   ∀i, k, n, a[0 ≤ n + 1 ∧ 0 ≤ k ∧ n + 1 ≤ i].
-   a → Array (a, i) → Num k → Num n → ∃k[0 ≤ k + 1 ∧
-     k ≤ n].Num k
+   ∀i, k, n, a[n + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n + 1].
+   a → Array (a, i) → Num k → Num n → ∃k[k ≤ n ∧
+     0 ≤ k + 1].Num k
 
 val bsearch :
    ∀n, a[0 ≤ n + 1].
-   a → Array (a, n + 1) → ∃k[0 ≤ k + 1 ∧ k ≤ n].Num k
+   a → Array (a, n + 1) → ∃k[k ≤ n ∧ 0 ≤ k + 1].Num k

examples/liquid_bsearch2_harder2.gadti.target

@@ -26,4 +26,4 @@ external val div2 : ∀n. Num (2 n) → Num n
 
 val bsearch :
    ∀n, a[0 ≤ n + 1].
-   a → Array (a, n + 1) → ∃k[0 ≤ k + 1 ∧ k ≤ n].Num k
+   a → Array (a, n + 1) → ∃k[k ≤ n ∧ 0 ≤ k + 1].Num k

examples/liquid_bsearch2_harder3.gadti.target

@@ -26,4 +26,4 @@ external val div2 : ∀n. Num (2 n) → Num n
 
 val bsearch :
    ∀n, a[0 ≤ n].
-   a → Array (a, n) → ∃k[0 ≤ k + 1 ∧ k + 1 ≤ n].Num k
+   a → Array (a, n) → ∃k[k + 1 ≤ n ∧ 0 ≤ k + 1].Num k

examples/liquid_bsearch2_harder3.ml.target

@@ -21,17 +21,17 @@ let compare : ('a -> 'a -> linOrder) =
 let equal : ('a -> 'a -> bool) = fun a b -> a = b
 let div2 : ((* 2 n *) num -> (* n *) num) = fun x -> x / 2
 type ex4 =
-  | Ex4 : (*∀'k, 'n[0 ≤ k + 1 ∧ k + 1 ≤ n].*)(* k *) num ->
+  | Ex4 : (*∀'k, 'n[k + 1 ≤ n ∧ 0 ≤ k + 1].*)(* k *) num ->
     (* n *) ex4
 type ex3 =
-  | Ex3 : (*∀'k, 'n[0 ≤ k + 1 ∧ k ≤ n].*)(* k *) num -> (* n *) ex3
+  | Ex3 : (*∀'k, 'n[k ≤ n ∧ 0 ≤ k + 1].*)(* k *) num -> (* n *) ex3
 let bsearch
   : type (*n*) a (*0 ≤ n*). (a -> (a (* n *)) array -> (* n *) ex4) =
   (fun key vec ->
     let Ex3 xcase =
     let rec look :
-    type (*i*) (*j*) (*k*) b (*0 ≤ k + 1 ∧ 0 ≤ i ∧
-    k + 1 ≤ j*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num ->
+    type (*i*) (*j*) (*k*) b (*k + 1 ≤ j ∧ 0 ≤ i ∧
+    0 ≤ k + 1*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num ->
                      (* k *) ex3)
     =
     (fun key vec lo hi ->

examples/liquid_bsearch2_simpler.gadti.target

@@ -25,6 +25,6 @@ external val equal : ∀a. a → a → Bool
 external val div2 : ∀n. Num (2 n) → Num n
 
 val look :
-   ∀i, k, n, a[0 ≤ k ∧ k ≤ n + 1 ∧ n + 1 ≤ i].
-   a → Array (a, i) → Num k → Num n → ∃k[0 ≤ k + 1 ∧
-     k ≤ n].Num k
+   ∀i, k, n, a[n + 1 ≤ i ∧ k ≤ n + 1 ∧ 0 ≤ k].
+   a → Array (a, i) → Num k → Num n → ∃k[k ≤ n ∧
+     0 ≤ k + 1].Num k

examples/liquid_fft.gadti.target

@@ -69,5 +69,5 @@ external val asgn : ∀a. Ref a → a → ()
 external val deref : ∀a. Ref a → a
 
 val fft :
-   ∀k, n[1 ≤ n ∧ n + 1 ≤ k].
+   ∀k, n[n + 1 ≤ k ∧ 1 ≤ n].
    Array (Float, n + 1) → Array (Float, k) → Num n

examples/liquid_fft_ffor.gadti.target

@@ -3,5 +3,5 @@ datatype Bounded : num * num
 datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k)
 
 val ffor :
-   ∀i, j, k, n[j ≤ i ∧ k ≤ n].
+   ∀i, j, k, n[k ≤ n ∧ j ≤ i].
    Num n → Num j → (Bounded (k, i) → ()) → ()

examples/liquid_fft_full.gadti.target

@@ -63,7 +63,7 @@ datatype Bounded : num * num
 datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k)
 
 val ffor :
-   ∀i, j, k, n[j ≤ i ∧ k ≤ n].
+   ∀i, j, k, n[k ≤ n ∧ j ≤ i].
    Num n → Num j → (Bounded (k, i) → ()) → ()
 
 external val ref : ∀a. a → Ref a
@@ -73,7 +73,7 @@ external val asgn : ∀a. Ref a → a → ()
 external val deref : ∀a. Ref a → a
 
 val fft :
-   ∀k, n[1 ≤ n ∧ n + 1 ≤ k].
+   ∀k, n[n + 1 ≤ k ∧ 1 ≤ n].
    Array (Float, n + 1) → Array (Float, k) → Num n
 
 val ffttest : ∀n[2 ≤ n]. Num n → Float

examples/liquid_fft_full_asserted.gadti.target

@@ -63,7 +63,7 @@ datatype Bounded : num * num
 datacons Index : ∀i, k, n[n ≤ i ∧ i ≤ k].Num i ⟶ Bounded (n, k)
 
 val ffor :
-   ∀i, j, k, n[j ≤ i ∧ k ≤ n].
+   ∀i, j, k, n[k ≤ n ∧ j ≤ i].
    Num n → Num j → (Bounded (k, i) → ()) → ()
 
 external val ref : ∀a. a → Ref a

examples/liquid_gauss.gadti.target

@@ -52,23 +52,23 @@ external val fl0 : Float
 external val fl1 : Float
 
 val getRow :
-   ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i].
+   ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, n) → Num k → Array (Float, n)
 
 val putRow :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j].
+   ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, j) → Num k → Array (Float, n) → ()
 
 val rowSwap :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
-   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+   ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧
+   0 ≤ n]. Matrix (i, j) → Num k → Num n → ()
 
 val norm :
-   ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i].
+   ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, i) → Num k → Num n → ()
 
 val rowElim :
-   ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
+   ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀k, n[0 ≤ n ∧ n ≤ k ∧ 1 ≤ k]. Matrix (n, k) → ()
+val gauss : ∀k, n[n ≤ k ∧ 1 ≤ n]. Matrix (n, k) → ()

examples/liquid_gauss2.gadti.target

@@ -52,23 +52,23 @@ external val fl0 : Float
 external val fl1 : Float
 
 val getRow :
-   ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i].
+   ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, n) → Num k → Array (Float, n)
 
 val putRow :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j].
+   ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, j) → Num k → Array (Float, n) → ()
 
 val rowSwap :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
-   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+   ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧
+   0 ≤ n]. Matrix (i, j) → Num k → Num n → ()
 
 val norm :
-   ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i].
+   ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, i) → Num k → Num n → ()
 
 val rowElim :
-   ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
+   ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()
+val gauss : ∀k, n[n + 1 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → ()

examples/liquid_gauss_asserted.gadti.target

@@ -52,23 +52,23 @@ external val fl0 : Float
 external val fl1 : Float
 
 val getRow :
-   ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i].
+   ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, n) → Num k → Array (Float, n)
 
 val putRow :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j].
+   ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, j) → Num k → Array (Float, n) → ()
 
 val rowSwap :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
-   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+   ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧
+   0 ≤ n]. Matrix (i, j) → Num k → Num n → ()
 
 val norm :
-   ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i].
+   ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, i) → Num k → Num n → ()
 
 val rowElim :
-   ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
+   ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
 val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()

examples/liquid_gauss_harder_asserted.gadti.target

@@ -52,23 +52,23 @@ external val fl0 : Float
 external val fl1 : Float
 
 val getRow :
-   ∀i, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i].
+   ∀i, k, n[k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, n) → Num k → Array (Float, n)
 
 val putRow :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n ≤ j].
+   ∀i, j, k, n[n ≤ j ∧ k + 1 ≤ i ∧ 0 ≤ k ∧ 0 ≤ n].
    Matrix (i, j) → Num k → Array (Float, n) → ()
 
 val rowSwap :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
-   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+   ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧
+   0 ≤ n]. Matrix (i, j) → Num k → Num n → ()
 
 val norm :
-   ∀i, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i].
+   ∀i, k, n[n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, i) → Num k → Num n → ()
 
 val rowElim :
-   ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
+   ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()
+val gauss : ∀k, n[n + 1 ≤ k ∧ 1 ≤ n]. Matrix (n, k) → ()

examples/liquid_gauss_rowElim.gadti.target

@@ -52,5 +52,5 @@ external val fl0 : Float
 external val fl1 : Float
 
 val rowElim :
-   ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
+   ∀i, j, k, n[k ≤ j ∧ n + 1 ≤ i ∧ k ≤ i ∧ 0 ≤ n].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()

examples/liquid_gauss_rowMax_2.gadti.target

@@ -68,8 +68,8 @@ external norm :
    Array (Float, i) → Num k → Num n → ()
 
 val rowMax :
-   ∀i, j, k, m, n[0 ≤ i ∧ i + 1 ≤ j ∧ i + 1 ≤ m ∧ 0 ≤ k ∧
-   0 ≤ n].
+   ∀i, j, k, m, n[0 ≤ n ∧ 0 ≤ k ∧ i + 1 ≤ m ∧ i + 1 ≤ j ∧
+   0 ≤ i].
    Matrix (j, m) → Num i →
      (Num k → Float → Num n → ∃k[0 ≤ k ∧
         k≤max (n, j + -1)].Num k,

examples/liquid_gauss_rowSwap.gadti.target

@@ -60,5 +60,5 @@ external putRow :
    Matrix (n, k) → Num i → Array (Float, j) → ()
 
 val rowSwap :
-   ∀i, j, k, n[0 ≤ n ∧ 0 ≤ k ∧ k + 1 ≤ i ∧ n + 1 ≤ i ∧
-   0 ≤ j]. Matrix (i, j) → Num k → Num n → ()
+   ∀i, j, k, n[0 ≤ j ∧ n + 1 ≤ i ∧ k + 1 ≤ i ∧ 0 ≤ k ∧
+   0 ≤ n]. Matrix (i, j) → Num k → Num n → ()

examples/liquid_gauss_simpler.gadti.target

@@ -71,4 +71,4 @@ external rowElim :
    ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀k, n[0 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()
+val gauss : ∀k, n[n + 1 ≤ k ∧ 0 ≤ n]. Matrix (n, k) → ()

examples/liquid_gauss_simpler_asserted.gadti.target

@@ -71,4 +71,4 @@ external rowElim :
    ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → ()

examples/liquid_heapsort.gadti.target

@@ -35,15 +35,15 @@ external val plus : Int → Int → Int
 external val int0 : Int
 
 val heapify :
-   ∀i, k, n, a[0 ≤ n ∧ i ≤ k].
+   ∀i, k, n, a[i ≤ k ∧ 0 ≤ n].
    Num i → Array (a, k) → Num n → ()
 
 val buildheap : ∀k, n, a[k ≤ n]. Num k → Array (a, n) → ()
 
 val heapsort :
-   ∀i, k, n, a[k ≤ n ∧ i ≤ k].
+   ∀i, k, n, a[i ≤ k ∧ k ≤ n].
    Num i → Num k → Array (a, n) → ()
 
 val print_array :
-   ∀i, k, n[k ≤ i ∧ 0 ≤ n].
+   ∀i, k, n[0 ≤ n ∧ k ≤ i].
    Array (String, i) → Num n → Num k → ()

examples/liquid_heapsort_heapify.gadti.target

@@ -35,5 +35,5 @@ external val plus : Int → Int → Int
 external val int0 : Int
 
 val heapify :
-   ∀i, k, n, a[0 ≤ n ∧ i ≤ k].
+   ∀i, k, n, a[i ≤ k ∧ 0 ≤ n].
    Num i → Array (a, k) → Num n → ()

examples/liquid_heapsort_heapify_simpler.gadti.target

@@ -35,5 +35,5 @@ external val plus : Int → Int → Int
 external val int0 : Int
 
 val heapify :
-   ∀i, k, n, a[0 ≤ n ∧ n + 1 ≤ i ∧ i ≤ k].
+   ∀i, k, n, a[i ≤ k ∧ n + 1 ≤ i ∧ 0 ≤ n].
    Num i → Array (a, k) → Num n → ()