Problem with Inequality Closure?

[DavePearce]

The following fails for reasons unknown:

type nat is (int x) where x >= 0

define update(int[] items, int[] nitems) is:
    forall(int k):
        if:
          k != 0
        then:
          items[k] == nitems[k]

assert:
    forall(nat[] xs, int[] ys, int j):
       if:
          |xs| == |ys|
          update(xs,ys)
          ys[0] == 1
       then:           
          ys[j] >= 0

Looking at the proof is helpful:

 133. exists(nat[] xs, int[] ys, int j).(update(xs, ys) && (1 == ys[0]) && ( () 
 150. update(xs, ys) && forall(int i:0).(nat(xs[i:0]) || (0 >= ( (Exists-E 133) 
 109. update(xs, ys)                                                (And-E 150) 
 149. forall(int i:0).(nat(xs[i:0]) || (0 >= (1 + i:0)) || (i:0 >= |xs|))       
 117. 1 == ys[0]                                                                
 124. |ys| == |xs|                                                              
 131. 0 >= (1 + ys[j])                                                          
 165. forall(int k).((0 == k) || (ys[k] == xs[k]))                (Macro-I 109) 
 170. forall(int i:0).((0 >= (1 + i:0)) || (i:0 >= |xs|) || (xs[i (Macro-I 149) 
 171. |xs| >= 1                                              (ArrIdx-I 124,117) 
 173. true                                                   (Forall-I 165,117) 
 175. |xs| >= (1 + j)                                        (ArrIdx-I 124,131) 
 176. j >= 0                                                 (ArrIdx-I 175,131) 
 183. (0 == j) || (ys[j] == xs[j])                           (Forall-I 165,131) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 177. 0 == j                                                       (Or-E 183) │
│ 185. 0 >= (1 + ys[0])                                         (Eq-S 131,177) │
├──────────────────────────────────────────────────────────────────────────────┤
│ 182. ys[j] == xs[j]                                               (Or-E 183) │
└──────────────────────────────────────────────────────────────────────────────┘

We can see that it's failing on the case where j == 0. This should be the easiest case! In particular, we can see 117. 1 == ys[0] so it should be no sweat.

UPDATE: possible construct is not recursive when it should be?

[DavePearce]

Right, the problem here is, again, representation. Basically, it's not moving the generated equation 0 >= (1 + us[0]) into normal form. This can be done with the following:

updatedTruth = Formulae.simplifyFormula(updatedTruth, types);
updatedTruth = (Formula) construct(state,updatedTruth);
updatedTruth = Formulae.simplifyFormula(updatedTruth, types);

But, at this point, it's fair to say that things are getting RIDICULOUS.