Definition: index-min
index-min(zs) ==
  rec-case(zs) of
  [] => <0, 0>
  z::more =>
   p.if more Ax then <0, z> otherwise let i,x 
                      in if (z) < (x)  then <0, z>  else eval in <j, x>

Lemma: index-min_wf
[zs:ℤ List+]. (index-min(zs) ∈ i:ℕ||zs|| × {x:ℤ(x zs[i] ∈ ℤ) ∧ (∀z:ℤ((z ∈ zs)  (x ≤ z)))} )

Definition: index-of-min
index-of-min(zs) ==  fst(index-min(zs))

Lemma: index-of-min_wf
[zs:ℤ List+]. (index-of-min(zs) ∈ {i:ℕ||zs||| ∀x:ℤ((x ∈ zs)  (zs[i] ≤ x))} )

Lemma: rev-append-property
[as,bs:Top].  (rev(as) bs rev(as) [] bs)

Lemma: rev-append-as-reverse
[as,bs:Top].  (rev(as) bs rev(as) bs)

Lemma: member-rev-append
[T:Type]. ∀x:T. ∀as,bs:T List.  ((x ∈ rev(as) bs) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))

Lemma: eager_product_map_nil_lemma
bs,f:Top.  (eager-product-map(f;[];bs) [])

Lemma: eager_product_map_cons_lemma
L,as,a,f:Top.  (eager-product-map(f;[a as];L) eager-map-append(f a;L;eager-product-map(f;as;L)))

Lemma: eager-product-map-nil
[f:Top]. ∀[as:Top List].  (eager-product-map(f;as;[]) [])

Lemma: l_all_eager_product-map
  ∀A,B:Type. ∀Pa:A ⟶ ℙ. ∀Pb:B ⟶ ℙ. ∀Pt:T ⟶ ℙ. ∀f:A ⟶ B ⟶ T.
    ((∀a:A. ∀b:B.  (Pa[a]  Pb[b]  Pt[f b]))
     (∀as:A List. ∀bs:B List.  ((∀a∈as.Pa[a])  (∀b∈bs.Pb[b])  (∀t∈eager-product-map(f;as;bs).Pt[t])))) 
  supposing value-type(T)

Lemma: map-map2
[as,f,g:Top].  (map(g;map(f;as)) map(g f;as))

Lemma: map-id-map
[as,f:Top].  (map(λx.x;map(f;as)) map(f;as))

Definition: accumulate_abort
accumulate_abort(x,sofar.F[x; sofar];s;L) ==  eager-accum(r, of inl(sofar) => F[x; sofar] inr(_) => r;s;L)

Lemma: accumulate_abort_wf
[A,B:Type]. ∀[s:B?]. ∀[F:A ⟶ B ⟶ (B?)]. ∀[L:A List].
  accumulate_abort(x,sofar.F[x;sofar];s;L) ∈ B? supposing valueall-type(B)

Lemma: accumulate_abort_nil_lemma
s,F:Top.  (accumulate_abort(x,y.F[x;y];s;[]) s)

Lemma: accumulate_abort_cons_lemma
  (accumulate_abort(x,y.F[x;y];s;[u v]) let s' ⟵ case of inl(y) => F[u;y] inr(_) => s
                                            in accumulate_abort(x,y.F[x;y];s';v))

Lemma: accumulate_abort-aborted
[z:Unit]. ∀[F:Top]. ∀[L:Top List].  (accumulate_abort(x,sofar.F[x;sofar];inr ;L) inr )

Lemma: assert-list-deq
[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List].  uiff(↑(list-deq(eq) as bs);as bs ∈ (A List))

Definition: integer-dot-product
as ⋅ bs
==r if as Ax then otherwise if bs Ax then otherwise let a,as2 as 
                                                            in let b,bs2 bs 
                                                               in (a b) as2 ⋅ bs2

Lemma: int_dot_nil_left_lemma
bs:Top. ([] ⋅ bs 0)

Lemma: int_dot_cons_nil_lemma
as,a:Top.  ([a as] ⋅ [] 0)

Lemma: int_dot_cons_lemma
bs,b,as,a:Top.  ([a as] ⋅ [b bs] (a b) as ⋅ bs)

Lemma: integer-dot-product_wf
[as,bs:ℤ List].  (as ⋅ bs ∈ ℤ)

Lemma: integer-dot-product-comm
[as,bs:ℤ List].  (as ⋅ bs bs ⋅ as)

Definition: satisfies-integer-equality
xs ⋅ as =0 ==  (||xs|| ||as|| ∈ ℤ) ∧ 0 < ||xs|| ∧ (hd(xs) 1 ∈ ℤ) ∧ (as ⋅ xs 0 ∈ ℤ)

Lemma: satisfies-integer-equality_wf
[xs,as:ℤ List].  (xs ⋅ as =0 ∈ ℙ)

Definition: satisfies-integer-inequality
xs ⋅ as ≥==  (||xs|| ||as|| ∈ ℤ) ∧ 0 < ||xs|| ∧ (hd(xs) 1 ∈ ℤ) ∧ (as ⋅ xs ≥ )

Lemma: satisfies-integer-inequality_wf
[xs,as:ℤ List].  (xs ⋅ as ≥0 ∈ ℙ)

Lemma: trivial-unsat-integer-inequality
[xs:ℤ List]. xs ⋅ [-1] ≥0)

Definition: list-delete
as\i==r if as Ax then as otherwise let a,as2 as in if (i) < (1)  then as2  else [a as2\i 1]

Lemma: list-delete_wf
[T:Type]. ∀[as:T List]. ∀[i:ℤ].  (as\i ∈ List)

Lemma: length-list-delete
[T:Type]. ∀[as:T List]. ∀[i:ℕ].  ||as\i|| (||as|| 1) ∈ ℤ supposing i < ||as||

Definition: int-vec-mul
as ==  map(λx.(a x);as)

Lemma: int-vec-mul_wf
[a:ℤ]. ∀[as:ℤ List].  (a as ∈ ℤ List)

Lemma: int-vec-mul-mul
[a,b:ℤ]. ∀[as:ℤ List].  (a as as)

Lemma: length-int-vec-mul
[a,as:Top].  (||a as|| ||as||)

Definition: int-vec-add
as bs
==r if as Ax then as otherwise if bs Ax then bs otherwise let a,as2 as 
                                                              in let b,bs2 bs 
                                                                 in [a as2 bs2]

Lemma: int-vec-add_wf
[as,bs:ℤ List].  (as bs ∈ ℤ List)

Lemma: length-int-vec-add
[as,bs:ℤ List].  ||as bs|| ||bs|| ∈ ℤ supposing ||as|| ||bs|| ∈ ℤ

Lemma: select-int-vec-add
[as,bs:ℤ List]. ∀[i:ℕ].  as bs[i] as[i] bs[i] supposing i < ||as|| ∧ i < ||bs||

Lemma: select-int-vec-mul
[x:ℤ]. ∀[as:ℤ List]. ∀[i:ℕ||as||].  (x as[i] as[i])

Lemma: int-dot-mul-left
[x:ℤ]. ∀[as,bs:ℤ List].  (x as ⋅ bs as ⋅ bs)

Lemma: int-dot-mul-right
[x:ℤ]. ∀[as,bs:ℤ List].  (as ⋅ bs as ⋅ bs)

Lemma: int-dot-add-left
[as,bs,cs:ℤ List].  as bs ⋅ cs as ⋅ cs bs ⋅ cs supposing ||as|| ||bs|| ∈ ℤ

Lemma: int-dot-add-right
[cs,as,bs:ℤ List].  cs ⋅ as bs cs ⋅ as cs ⋅ bs supposing ||as|| ||bs|| ∈ ℤ

Lemma: int-dot-select
[as,bs:ℤ List]. ∀[i:ℕ].  as ⋅ bs (as[i] bs[i]) as\i ⋅ bs\i supposing i < ||as|| ∧ i < ||bs||

Lemma: int-dot-reduce-dim
[as,bs:ℤ List]. ∀[i:ℕ].
  ∀[cs:ℤ List]. (as ⋅ bs as[i] cs as\i ⋅ bs\i) supposing ((bs[i] cs ⋅ bs\i ∈ ℤand (||cs|| (||as|| 1) ∈ ℤ))\000C 
  supposing i < ||as|| ∧ i < ||bs||

Lemma: int-eq-constraint-factor
[a:ℤ]. ∀[g:ℤ-o]. ∀[xs,L:ℤ List].
  uiff([1 xs] ⋅ [a L] 0 ∈ ℤ;((a rem g) 0 ∈ ℤ) ∧ ([1 xs] ⋅ [a ÷ L] 0 ∈ ℤ))

Lemma: int-eq-constraint-factor-sym
[a:ℤ]. ∀[g:ℤ-o]. ∀[xs,L:ℤ List].
  uiff([a L] ⋅ [1 xs] 0 ∈ ℤ;((a rem g) 0 ∈ ℤ) ∧ ([a ÷ L] ⋅ [1 xs] 0 ∈ ℤ))

Lemma: int-ineq-constraint-factor
[a:ℤ]. ∀[g:ℕ+]. ∀[xs,L:ℤ List].  uiff(0 ≤ [1 xs] ⋅ [a L];0 ≤ [1 xs] ⋅ [a ÷↓ L])

Lemma: int-ineq-constraint-factor-sym
[a:ℤ]. ∀[g:ℕ+]. ∀[xs,L:ℤ List].  uiff(0 ≤ [a L] ⋅ [1 xs];0 ≤ [a ÷↓ L] ⋅ [1 xs])

Lemma: gcd-list-property
L:ℤ List+
  ((∃R:ℤ List. (L gcd-list(L) R ∈ (ℤ List))) ∧ (∃S:ℤ List. ((||S|| ||L|| ∈ ℤ) ∧ (gcd-list(L) S ⋅ L ∈ ℤ))))

Definition: shadow-vec
shadow-vec(i;as;bs) ==
  eval bs' evalall(as[i] bs) in
  eval as' evalall(-bs[i] as) in
  eval evalall(bs' as') in

Lemma: shadow-vec_wf
[as,bs:ℤ List]. ∀[i:ℕ||as||].  shadow-vec(i;as;bs) ∈ ℤ List supposing ||as|| ||bs|| ∈ ℤ

Lemma: length-shadow-vec
[as,bs:ℤ List]. ∀[i:ℕ||as||].  ||shadow-vec(i;as;bs)|| (||as|| 1) ∈ ℤ supposing ||as|| ||bs|| ∈ ℤ

Lemma: shadow-vec-property
[as,bs:ℤ List]. ∀[i:ℕ||as||].
  (∀[xs:ℤ List]
     0 ≤ shadow-vec(i;as;bs) ⋅ xs\i supposing (||xs|| ||as|| ∈ ℤ) ∧ (0 ≤ as ⋅ xs) ∧ (0 ≤ bs ⋅ xs)) supposing 
     ((bs[i] ≤ 0) and 
     (0 ≤ as[i]) and 
     (||as|| ||bs|| ∈ ℤ))

Definition: int_termco
int_termco() ==
  corec(X.lbl:Atom × if lbl =a "Constant" then ℤ
                     if lbl =a "Var" then ℤ
                     if lbl =a "Add" then left:X × X
                     if lbl =a "Subtract" then left:X × X
                     if lbl =a "Multiply" then left:X × X
                     if lbl =a "Minus" then X
                     else Void
                     fi )

Lemma: int_termco_wf
int_termco() ∈ Type

Lemma: int_termco-ext
int_termco() ≡ lbl:Atom × if lbl =a "Constant" then ℤ
                          if lbl =a "Var" then ℤ
                          if lbl =a "Add" then left:int_termco() × int_termco()
                          if lbl =a "Subtract" then left:int_termco() × int_termco()
                          if lbl =a "Multiply" then left:int_termco() × int_termco()
                          if lbl =a "Minus" then int_termco()
                          else Void

Definition: int_termco_size
int_termco_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "Constant" then 0
                   if lbl =a "Var" then 0
                   if lbl =a "Add" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "Subtract" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "Multiply" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "Minus" then (size x)
                   else 0
                   fi )) 

Lemma: int_termco_size_wf
[p:int_termco()]. (int_termco_size(p) ∈ partial(ℕ))

Definition: int_term
int_term() ==  {p:int_termco()| (int_termco_size(p))↓

Lemma: int_term_wf
int_term() ∈ Type

Definition: int_term_size
int_term_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "Constant" then 0
                   if lbl =a "Var" then 0
                   if lbl =a "Add" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "Subtract" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "Multiply" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "Minus" then (size x)
                   else 0
                   fi )) 

Lemma: int_term_size_wf
[p:int_term()]. (int_term_size(p) ∈ ℕ)

Lemma: int_term-ext
int_term() ≡ lbl:Atom × if lbl =a "Constant" then ℤ
                        if lbl =a "Var" then ℤ
                        if lbl =a "Add" then left:int_term() × int_term()
                        if lbl =a "Subtract" then left:int_term() × int_term()
                        if lbl =a "Multiply" then left:int_term() × int_term()
                        if lbl =a "Minus" then int_term()
                        else Void

Definition: itermConstant
"const" ==  <"Constant", const>

Lemma: itermConstant_wf
[const:ℤ]. ("const" ∈ int_term())

Definition: itermVar
vvar ==  <"Var", var>

Lemma: itermVar_wf
[var:ℤ]. (vvar ∈ int_term())

Definition: itermAdd
left (+) right ==  <"Add", left, right>

Lemma: itermAdd_wf
[left,right:int_term()].  (left (+) right ∈ int_term())

Definition: itermSubtract
left (-) right ==  <"Subtract", left, right>

Lemma: itermSubtract_wf
[left,right:int_term()].  (left (-) right ∈ int_term())

Definition: itermMultiply
left (*) right ==  <"Multiply", left, right>

Lemma: itermMultiply_wf
[left,right:int_term()].  (left (*) right ∈ int_term())

Definition: itermMinus
"-"num ==  <"Minus", num>

Lemma: itermMinus_wf
[num:int_term()]. ("-"num ∈ int_term())

Definition: itermConstant?
itermConstant?(v) ==  fst(v) =a "Constant"

Lemma: itermConstant?_wf
[v:int_term()]. (itermConstant?(v) ∈ 𝔹)

Definition: itermConstant-const
itermConstant-const(v) ==  snd(v)

Lemma: itermConstant-const_wf
[v:int_term()]. itermConstant-const(v) ∈ ℤ supposing ↑itermConstant?(v)

Definition: itermVar?
itermVar?(v) ==  fst(v) =a "Var"

Lemma: itermVar?_wf
[v:int_term()]. (itermVar?(v) ∈ 𝔹)

Definition: itermVar-var
itermVar-var(v) ==  snd(v)

Lemma: itermVar-var_wf
[v:int_term()]. itermVar-var(v) ∈ ℤ supposing ↑itermVar?(v)

Definition: itermAdd?
itermAdd?(v) ==  fst(v) =a "Add"

Lemma: itermAdd?_wf
[v:int_term()]. (itermAdd?(v) ∈ 𝔹)

Definition: itermAdd-left
itermAdd-left(v) ==  fst(snd(v))

Lemma: itermAdd-left_wf
[v:int_term()]. itermAdd-left(v) ∈ int_term() supposing ↑itermAdd?(v)

Definition: itermAdd-right
itermAdd-right(v) ==  snd(snd(v))

Lemma: itermAdd-right_wf
[v:int_term()]. itermAdd-right(v) ∈ int_term() supposing ↑itermAdd?(v)

Definition: itermSubtract?
itermSubtract?(v) ==  fst(v) =a "Subtract"

Lemma: itermSubtract?_wf
[v:int_term()]. (itermSubtract?(v) ∈ 𝔹)

Definition: itermSubtract-left
itermSubtract-left(v) ==  fst(snd(v))

Lemma: itermSubtract-left_wf
[v:int_term()]. itermSubtract-left(v) ∈ int_term() supposing ↑itermSubtract?(v)

Definition: itermSubtract-right
itermSubtract-right(v) ==  snd(snd(v))

Lemma: itermSubtract-right_wf
[v:int_term()]. itermSubtract-right(v) ∈ int_term() supposing ↑itermSubtract?(v)

Definition: itermMultiply?
itermMultiply?(v) ==  fst(v) =a "Multiply"

Lemma: itermMultiply?_wf
[v:int_term()]. (itermMultiply?(v) ∈ 𝔹)

Definition: itermMultiply-left
itermMultiply-left(v) ==  fst(snd(v))

Lemma: itermMultiply-left_wf
[v:int_term()]. itermMultiply-left(v) ∈ int_term() supposing ↑itermMultiply?(v)

Definition: itermMultiply-right
itermMultiply-right(v) ==  snd(snd(v))

Lemma: itermMultiply-right_wf
[v:int_term()]. itermMultiply-right(v) ∈ int_term() supposing ↑itermMultiply?(v)

Definition: itermMinus?
itermMinus?(v) ==  fst(v) =a "Minus"

Lemma: itermMinus?_wf
[v:int_term()]. (itermMinus?(v) ∈ 𝔹)

Definition: itermMinus-num
itermMinus-num(v) ==  snd(v)

Lemma: itermMinus-num_wf
[v:int_term()]. itermMinus-num(v) ∈ int_term() supposing ↑itermMinus?(v)

Lemma: int_term-induction
[P:int_term() ⟶ ℙ]
   (∀left,right:int_term().  (P[left]  P[right]  P[left (+) right]))
   (∀left,right:int_term().  (P[left]  P[right]  P[left (-) right]))
   (∀left,right:int_term().  (P[left]  P[right]  P[left (*) right]))
   (∀num:int_term(). (P[num]  P["-"num]))
   {∀v:int_term(). P[v]})

Lemma: int_term-definition
[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ].
  ((∀const:ℤ{x:A| R[x;"const"]} )
   (∀var:ℤ{x:A| R[x;vvar]} )
   (∀left,right:int_term().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;left (+) right]} ))
   (∀left,right:int_term().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;left (-) right]} ))
   (∀left,right:int_term().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;left (*) right]} ))
   (∀num:int_term(). ({x:A| R[x;num]}   {x:A| R[x;"-"num]} ))
   {∀v:int_term(). {x:A| R[x;v]} })

Definition: int_term_ind
             itermConstant(const) Constant[const];
             itermVar(var) Var[var];
             itermAdd(left,right) rec1,rec2.Add[left;
             itermSubtract(left,right) rec3,rec4.Subtract[left;
             itermMultiply(left,right) rec5,rec6.Multiply[left;
             itermMinus(num) rec7.Minus[num; rec7])  ==
  fix((λint_term_ind,v. let lbl,v1 
                        in if lbl="Constant" then Constant[v1]
                           if lbl="Var" then Var[v1]
                           if lbl="Add"
                             then let left,v2 v1 
                                  in Add[left;
                                         int_term_ind left;
                                         int_term_ind v2]
                           if lbl="Subtract"
                             then let left,v2 v1 
                                  in Subtract[left;
                                              int_term_ind left;
                                              int_term_ind v2]
                           if lbl="Multiply"
                             then let left,v2 v1 
                                  in Multiply[left;
                                              int_term_ind left;
                                              int_term_ind v2]
                           if lbl="Minus" then Minus[v1; int_term_ind v1]
                           else Ax
                           fi )) 

Lemma: int_term_ind_wf
[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ]. ∀[v:int_term()]. ∀[Constant:const:ℤ ⟶ {x:A| R[x;"const"]} ].
[Var:var:ℤ ⟶ {x:A| R[x;vvar]} ]. ∀[Add:left:int_term()
                                        ⟶ right:int_term()
                                        ⟶ {x:A| R[x;left]} 
                                        ⟶ {x:A| R[x;right]} 
                                        ⟶ {x:A| R[x;left (+) right]} ]. ∀[Subtract:left:int_term()
                                                                                   ⟶ right:int_term()
                                                                                   ⟶ {x:A| R[x;left]} 
                                                                                   ⟶ {x:A| R[x;right]} 
                                                                                   ⟶ {x:A| R[x;left (-) right]} ].
[Multiply:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left (*) right]} \000C].
[Minus:num:int_term() ⟶ {x:A| R[x;num]}  ⟶ {x:A| R[x;"-"num]} ].
                itermConstant(const) Constant[const];
                itermVar(var) Var[var];
                itermAdd(left,right) rec1,rec2.Add[left;right;rec1;rec2];
                itermSubtract(left,right) rec3,rec4.Subtract[left;right;rec3;rec4];
                itermMultiply(left,right) rec5,rec6.Multiply[left;right;rec5;rec6];
                itermMinus(num) rec7.Minus[num;rec7])  ∈ {x:A| R[x;v]} )

Lemma: int_term_ind_wf_simple
[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
                                                                                ⟶ right:int_term()
                                                                                ⟶ A
                                                                                ⟶ A
                                                                                ⟶ A].
[Minus:num:int_term() ⟶ A ⟶ A].
                itermConstant(const) Constant[const];
                itermVar(var) Var[var];
                itermAdd(left,right) rec1,rec2.Add[left;right;rec1;rec2];
                itermSubtract(left,right) rec3,rec4.Subtract[left;right;rec3;rec4];
                itermMultiply(left,right) rec5,rec6.Multiply[left;right;rec5;rec6];
                itermMinus(num) rec7.Minus[num;rec7])  ∈ A)

Lemma: int_term_subtype_base
int_term() ⊆Base

Definition: int-term-ind-fun
                 x,rx.MN[x; rx]) ==
                  itermConstant(c) C[c];
                  itermVar(v) V[v];
                  itermAdd(l,r) rl,rr.A[l;
                  itermSubtract(l,r) rl,rr.S[l;
                  itermMultiply(l,r) rl,rr.M[l;
                  itermMinus(x) rx.MN[x; rx]) 

Lemma: int-term-ind-fun_wf
[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
                                                                                ⟶ right:int_term()
                                                                                ⟶ A
                                                                                ⟶ A
                                                                                ⟶ A].
[Minus:num:int_term() ⟶ A ⟶ A].
                    x,rx.Minus[x;rx]) ∈ int_term() ⟶ A)

Lemma: int_term_ind-var
   vk V[k])

Lemma: int_term_ind-const
   "c" C[c])

Lemma: int_term_ind-add
   (a (+) b) A[a;b;int-term-ind-fun(c.C[c];

Lemma: int_term_ind-sub
   (a (-) b) S[a;b;int-term-ind-fun(c.C[c];

Lemma: int_term_ind-mul
   (a (*) b) M[a;b;int-term-ind-fun(c.C[c];

Lemma: int_term_ind-minus
   "-"x MN[x;int-term-ind-fun(c.C[c];

Definition: int_term_value
int_term_value(f;t) ==
               itermConstant(n) n;
               itermVar(v) v;
               itermAdd(l,r) rl,rr.rl rr;
               itermSubtract(l,r) rl,rr.rl rr;
               itermMultiply(l,r) rl,rr.rl rr;
               itermMinus(x) r.-r) 

Lemma: int_term_value_wf
[f:ℤ ⟶ ℤ]. ∀[t:int_term()].  (int_term_value(f;t) ∈ ℤ)

Lemma: int_term_value_add_lemma
y,x,f:Top.  (int_term_value(f;x (+) y) int_term_value(f;x) int_term_value(f;y))

Lemma: int_term_value_mul_lemma
y,x,f:Top.  (int_term_value(f;x (*) y) int_term_value(f;x) int_term_value(f;y))

Lemma: int_term_value_subtract_lemma
y,x,f:Top.  (int_term_value(f;x (-) y) int_term_value(f;x) int_term_value(f;y))

Lemma: int_term_value_minus_lemma
x,f:Top.  (int_term_value(f;"-"x) -int_term_value(f;x))

Lemma: int_term_value_constant_lemma
x,f:Top.  (int_term_value(f;"x") x)

Lemma: int_term_value_var_lemma
x,f:Top.  (int_term_value(f;vx) x)

Definition: equiv_int_terms
t1 ≡ t2 ==  ∀f:ℤ ⟶ ℤ(int_term_value(f;t1) int_term_value(f;t2) ∈ ℤ)

Lemma: equiv_int_terms_wf
[t1,t2:int_term()].  (t1 ≡ t2 ∈ ℙ)

Lemma: equiv_int_terms_weakening
[t1,t2:int_term()].  t1 ≡ t2 supposing t1 t2 ∈ int_term()

Lemma: equiv_int_terms_transitivity
[t1,t2,t3:int_term()].  (t1 ≡ t3) supposing (t2 ≡ t3 and t1 ≡ t2)

Lemma: equiv_int_terms_inversion
[t1,t2:int_term()].  t1 ≡ t2 supposing t2 ≡ t1

Lemma: equiv_int_terms_functionality
[x1,x2,y1,y2:int_term()].  (uiff(x1 ≡ y1;x2 ≡ y2)) supposing (y1 ≡ y2 and x1 ≡ x2)

Lemma: int_term_value_functionality
[f:ℤ ⟶ ℤ]. ∀[t1,t2:int_term()].  int_term_value(f;t1) int_term_value(f;t2) ∈ ℤ supposing t1 ≡ t2

Lemma: itermAdd_functionality
[a,b,c,d:int_term()].  (a (+) c ≡ (+) d) supposing (a ≡ and c ≡ d)

Lemma: itermSubtract_functionality
[a,b,c,d:int_term()].  (a (-) c ≡ (-) d) supposing (a ≡ and c ≡ d)

Lemma: itermMultiply_functionality
[a,b,c,d:int_term()].  (a (*) c ≡ (*) d) supposing (a ≡ and c ≡ d)

Lemma: itermMinus_functionality
[a,b:int_term()].  "-"a ≡ "-"b supposing a ≡ b

Definition: iMonomial
iMonomial() ==  ℤ-o × {vs:ℤ List| sorted(vs)} 

Lemma: iMonomial_wf
iMonomial() ∈ Type

Definition: isMonomialOne
isMonomialOne(m) ==  let a,vs in null(vs) ∧b (a =z 1)

Lemma: isMonomialOne_wf
[m:iMonomial()]. (isMonomialOne(m) ∈ 𝔹)

Lemma: iMonomial-value-type

Definition: imonomial-le
imonomial-le(m1;m2) ==  snd(m1) ≤_lex snd(m2)

Lemma: imonomial-le_wf
[m1,m2:iMonomial()].  (imonomial-le(m1;m2) ∈ 𝔹)

Definition: imonomial-less
imonomial-less(m1;m2) ==  ((snd(m1)) (snd(m2)) ∈ (ℤ List))) ∧ (↑imonomial-le(m1;m2))

Lemma: imonomial-less_wf
[m1,m2:iMonomial()].  (imonomial-less(m1;m2) ∈ ℙ)

Lemma: imonomial-less-transitive
[m1,m2,m3:iMonomial()].  (imonomial-less(m1;m3)) supposing (imonomial-less(m2;m3) and imonomial-less(m1;m2))

Lemma: not-imonomial-le
a,b:iMonomial().  ((¬↑imonomial-le(a;b))  imonomial-less(b;a))

Definition: iPolynomial
iPolynomial() ==  {L:iMonomial() List| ∀i:ℕ||L||. ∀j:ℕi.  imonomial-less(L[j];L[i])} 

Lemma: iPolynomial_wf
iPolynomial() ∈ Type

Definition: isPolyOne
isPolyOne(p) ==  if is pair then let m,more in null(more) ∧b isMonomialOne(m) otherwise ff

Lemma: isPolyOne_wf
[p:iPolynomial()]. (isPolyOne(p) ∈ 𝔹)

Definition: imonomial-term
imonomial-term(m) ==
  let c,vs 
  in accumulate (with value and list item v):
      (*) vv
     over list:
     with starting value:

Lemma: imonomial-term_wf
[m:ℤ × (ℤ List)]. (imonomial-term(m) ∈ int_term())

Lemma: imonomial-cons
v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u v]>)) int_term_value(f;imonomial-term(<(f\000C u), v>)) ∈ ℤ)

Lemma: imonomial-term-linear
f:ℤ ⟶ ℤ. ∀ws:ℤ List. ∀c:ℤ.  (int_term_value(f;imonomial-term(<c, ws>)) (c int_term_value(f;imonomial-term(<1, ws>)\000C)) ∈ ℤ)

Lemma: imonomial-term-add
vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ ℤ.  ((int_term_value(f;imonomial-term(<a, vs>)) int_term_value(f;imonomial-term(<b, vs>)\000C)) int_term_value(f;imonomial-term(<b, vs>)) ∈ ℤ)

Definition: ipolynomial-term
ipolynomial-term(p) ==
  if null(p)
  then "0"
  else let m1,ms 
       in accumulate (with value and list item m):
           (+) imonomial-term(m)
          over list:
          with starting value:

Lemma: ipolynomial-term_wf
[p:iMonomial() List]. (ipolynomial-term(p) ∈ int_term())

Lemma: ipolynomial-term-cons
[m:iMonomial()]. ∀[p:iMonomial() List].  ipolynomial-term([m p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)

Lemma: ipolynomial-term-cons-value
[m:iMonomial()]. ∀[p:iMonomial() List].
  ∀f:ℤ ⟶ ℤ
    (int_term_value(f;ipolynomial-term([m p]))
    (int_term_value(f;imonomial-term(m)) int_term_value(f;ipolynomial-term(p)))
    ∈ ℤ)

Definition: add-ipoly
==r eval pp in
    eval qq in
      if null(pp) then qq
      if null(qq) then pp
      else let p1,ps pp 
           in let q1,qs qq 
              in if imonomial-le(p1;q1)
                 then if imonomial-le(q1;p1)
                      then let x ⟵ add-ipoly(ps;qs)
                           in let cp,vs p1 
                              in eval cp (fst(q1)) in
                                 if c=0 then else [<c, vs> x]
                      else let x ⟵ add-ipoly(ps;[q1 qs])
                           in [p1 x]
                 else let x ⟵ add-ipoly([p1 ps];qs)
                      in [q1 x]

Lemma: add-ipoly_wf1
[p,q:iMonomial() List].  (add-ipoly(p;q) ∈ iMonomial() List)

Definition: add-ipoly1
add-ipoly1(p;q) ==  add-ipoly(p;q)

Lemma: add-poly-lemma1
p,q:iMonomial() List. ∀m:iMonomial().
  ((∀i:ℕ||p||. ∀j:ℕi.  imonomial-less(p[j];p[i]))
   (∀i:ℕ||q||. ∀j:ℕi.  imonomial-less(q[j];q[i]))
   (0 < ||p||  imonomial-less(m;p[0]))
   (0 < ||q||  imonomial-less(m;q[0]))
   0 < ||add-ipoly(p;q)||

Lemma: add-ipoly-equiv
p,q:iMonomial() List.  ipolynomial-term(add-ipoly(p;q)) ≡ ipolynomial-term(p) (+) ipolynomial-term(q)

Lemma: add-ipoly_wf
[p,q:iPolynomial()].  (add-ipoly(p;q) ∈ iPolynomial())

Definition: add-ipoly-prepend
==r eval pp in
    eval qq in
      if pp Ax then rev(l) qq
      otherwise if qq Ax then rev(l) pp otherwise let p1,ps pp 
                                                      in let q1,qs qq 
                                                         in if imonomial-le(p1;q1)
                                                            then if imonomial-le(q1;p1)
                                                                 then let cp,vs p1 
                                                                      in eval cp (fst(q1)) in
                                                                         eval l' if c=0 then else [<c, vs> l] in
                                                                 else add-ipoly-prepend(ps;[q1 qs];[p1 l])
                                                            else add-ipoly-prepend([p1 ps];qs;[q1 l])

Lemma: add-ipoly-wf1
p,q:(ℤ × (ℤ List)) List.  (add-ipoly(p;q) ∈ (ℤ × (ℤ List)) List)

Lemma: add-ipoly1_wf
p,q:(ℤ × (ℤ List)) List.  (add-ipoly1(p;q) ∈ (ℤ × (ℤ List)) List)

Lemma: add-poly-prepend-sq1
[p,q,l:(ℤ × (ℤ List)) List].  (add-ipoly-prepend(p;q;l) rev(l) add-ipoly(p;q))

Lemma: add-poly-prepend-sq
[p,q,l:iMonomial() List].  (add-ipoly-prepend(p;q;l) rev(l) add-ipoly(p;q))

Lemma: add-ipoly-prepend_wf
[p,q,l:iMonomial() List].  (add-ipoly-prepend(p;q;l) ∈ iMonomial() List)

Definition: add_ipoly
add_ipoly(p;q) ==  add-ipoly-prepend(p;q;[])

Lemma: add_ipoly-sq
[p,q:iMonomial() List].  (add_ipoly(p;q) add-ipoly(p;q))

Lemma: add_ipoly_wf
[p,q:iPolynomial()].  (add_ipoly(p;q) ∈ iPolynomial())

Definition: minus-monomial
minus-monomial(m) ==  let c,vs in <-c, vs>

Lemma: minus-monomial_wf
[m:iMonomial()]. (minus-monomial(m) ∈ iMonomial())

Definition: minus-poly
minus-poly(p) ==  map(λm.minus-monomial(m);p)

Lemma: minus-poly_wf
[p:iPolynomial()]. (minus-poly(p) ∈ iPolynomial())

Lemma: minus-poly-equiv
p:iPolynomial(). ipolynomial-term(minus-poly(p)) ≡ "-"ipolynomial-term(p)

Definition: mul-monomials
mul-monomials(m1;m2) ==  let a,vs m1 in let b,ws m2 in eval in eval merge-int-accum(vs;ws) in   <c, u>

Lemma: mul-monomials_wf
[m1,m2:iMonomial()].  (mul-monomials(m1;m2) ∈ iMonomial())

Lemma: mul-monomials-equiv
[m1,m2:iMonomial()].  imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)

Definition: even-int-list
even-int-list(L) ==  null(L) ∨b((¬bnull(tl(L))) ∧b (hd(L) =z hd(tl(L))) ∧b even-int-list(tl(tl(L))))

Lemma: even-int-list_wf
[L:ℤ List]. (even-int-list(L) ∈ 𝔹)

Definition: nonneg-monomial
nonneg-monomial(m) ==  let c,L in 0 ≤c ∧b even-int-list(L)

Lemma: nonneg-monomial_wf
[m:iMonomial()]. (nonneg-monomial(m) ∈ 𝔹)

Lemma: assert-nonneg-monomial
m:iMonomial(). ((↑nonneg-monomial(m))  (∃m':iMonomial(). ∃k:ℕ+(mul-monomials(m';m') mul-monomials(m;<k, []>) ∈ iM\000Conomial())))

Definition: mul-mono-poly
mul-mono-poly(m;p) ==  rec-case(p) of [] => [] h::t => r.eval mul-monomials(m;h) in eval in   [m l]

Lemma: mul-mono-poly_wf1
[m:iMonomial()]. ∀[p:iMonomial() List].  (mul-mono-poly(m;p) ∈ iMonomial() List)

Lemma: mul-mono-poly_wf
[m:iMonomial()]. ∀[p:iPolynomial()].  (mul-mono-poly(m;p) ∈ iPolynomial())

Lemma: mul-mono-poly-equiv
[m:iMonomial()]. ∀[p:iMonomial() List].
  ipolynomial-term(mul-mono-poly(m;p)) ≡ imonomial-term(m) (*) ipolynomial-term(p)

Definition: mul-ipoly
mul-ipoly(p;q) ==
  let pp ⟵ p
  in if null(pp)
  then []
  else let p1,ps pp 
       in let qq ⟵ q
          in if null(qq)
          then []
          else eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;qq));mul-mono-poly(p1;qq);ps)

Lemma: mul-ipoly_wf
[p,q:iPolynomial()].  (mul-ipoly(p;q) ∈ iPolynomial())

Lemma: mul-ipoly-equiv
[p,q:iMonomial() List].  ipolynomial-term(mul-ipoly(p;q)) ≡ ipolynomial-term(p) (*) ipolynomial-term(q)

Definition: cbv_list_accum
cbv_list_accum(x,a.f[x; a];y;L) ==
  fix((λcbv_list_accum,y,L. eval in
                            if is pair then let h,t 
                                                in eval y' f[y; h] in
                                                   cbv_list_accum y' otherwise if Ax then otherwise ⊥)) 

Lemma: cbv_list_accum_wf
[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].  cbv_list_accum(x,a.f[x;a];y;l) ∈ T' supposing value-type(T')

Lemma: cbv_list_accum-is-list_accum
[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].
  cbv_list_accum(x,a.f[x;a];y;l) accumulate (with value and list item a):
                                   over list:
                                   with starting value:
  supposing value-type(T')

Definition: mul_ipoly
mul_ipoly(p;q) ==
  eval pp in
  if pp Ax then []
  otherwise let p1,ps pp 
            in eval qq in
               if qq Ax then []
               otherwise cbv_list_accum(sofar,m.add_ipoly(sofar;mul-mono-poly(m;qq));mul-mono-poly(p1;qq);ps)

Lemma: mul_poly-sq
[p,q:iMonomial() List].  (mul_ipoly(p;q) mul-ipoly(p;q))

Lemma: mul_ipoly_wf
[p,q:iPolynomial()].  (mul_ipoly(p;q) ∈ iPolynomial())

Definition: int_term_to_ipoly
int_term_to_ipoly(t) ==
               itermConstant(c) if c=0 then [] else [<c, []>];
               itermVar(v) [<1, [v]>];
               itermAdd(l,r) rl,rr.add_ipoly(rl;rr);
               itermSubtract(l,r) rl,rr.add_ipoly(rl;minus-poly(rr));
               itermMultiply(l,r) rl,rr.mul_ipoly(rl;rr);
               itermMinus(x) rx.minus-poly(rx)) 

Lemma: int_term_to_ipoly_wf
[t:int_term()]. (int_term_to_ipoly(t) ∈ iPolynomial())

Definition: int_term_to_rP
int_term_to_rP(t) ==
               itermConstant(c) [1; c];
               itermVar(v) [2; v];
               itermAdd(l,r) rl,rr.eager-append(rl;eager-append(rr;[3]));
               itermSubtract(l,r) rl,rr.eager-append(rl;eager-append(rr;[4]));
               itermMultiply(l,r) rl,rr.eager-append(rl;eager-append(rr;[5]));
               itermMinus(x) rx.eager-append(rx;[6])) 

Lemma: int_term_to_rP_wf
[t:int_term()]. (int_term_to_rP(t) ∈ ℤ List)

Definition: rP_to_poly
==r if Ax then stack otherwise let op,more 
                                   in if op=1
                                      then let c,evenmore more 
                                           in rP_to_poly([if c=0 then [] else [<c, []>stack];evenmore)
                                      else if op=2
                                           then let v,evenmore more 
                                                in rP_to_poly(<[<1, [v]>], stack>;evenmore)
                                           else if op=3
                                                then let q,p,s stack in 
                                                     rP_to_poly([add_ipoly(p;q) s];more)
                                                else if op=4
                                                     then let q,p,s stack in 
                                                          rP_to_poly([add_ipoly(p;minus-poly(q)) s];more)
                                                     else if op=5
                                                          then let q,p,s stack in 
                                                               rP_to_poly([mul_ipoly(p;q) s];more)
                                                          else let p,s stack 
                                                               in rP_to_poly([minus-poly(p) s];more)

Lemma: rP_to_poly-int_term_to_rP
[t:int_term()]. ∀[s:iPolynomial() List].  (rP_to_poly(s;int_term_to_rP(t)) [int_term_to_ipoly(t) s])

Definition: rP_to_term
==r if Ax then stack otherwise let op,more 
                                   in if op=1
                                      then let c,evenmore more 
                                           in rP_to_term(["c" stack];evenmore)
                                      else if op=2
                                           then let v,evenmore more 
                                                in rP_to_term([vv stack];evenmore)
                                           else if op=3
                                                then let q,p,s stack in 
                                                     rP_to_term([p (+) s];more)
                                                else if op=4
                                                     then let q,p,s stack in 
                                                          rP_to_term([p (-) s];more)
                                                     else if op=5
                                                          then let q,p,s stack in 
                                                               rP_to_term([p (*) s];more)
                                                          else let p,s stack 
                                                               in rP_to_term(["-"p s];more)

Lemma: rP_to_term-int_term_to_rP
[t:int_term()]. ∀[s:int_term() List].  (rP_to_term(s;int_term_to_rP(t)) [t s])

Lemma: int_term_to_ipoly-add
[a,b:Top].  (int_term_to_ipoly(a (+) b) add_ipoly(int_term_to_ipoly(a);int_term_to_ipoly(b)))

Lemma: int_term_to_ipoly-sub
[a,b:Top].  (int_term_to_ipoly(a (-) b) add_ipoly(int_term_to_ipoly(a);minus-poly(int_term_to_ipoly(b))))

Lemma: int_term_to_ipoly-minus
[b:Top]. (int_term_to_ipoly("-"b) minus-poly(int_term_to_ipoly(b)))

Lemma: int_term_to_ipoly-mul
[a,b:Top].  (int_term_to_ipoly(a (*) b) mul_ipoly(int_term_to_ipoly(a);int_term_to_ipoly(b)))

Lemma: int_term_to_ipoly-const
[c:Top]. (int_term_to_ipoly("c") if c=0 then [] else [<c, []>])

Lemma: int_term_to_ipoly-var
[c:Top]. (int_term_to_ipoly(vc) [<1, [c]>])

Lemma: int_term_polynomial
t:int_term(). ipolynomial-term(int_term_to_ipoly(t)) ≡ t

Definition: const-poly
const-poly(n) ==  [<n, []>]

Lemma: const-poly_wf
[n:ℤ-o]. (const-poly(n) ∈ iPolynomial())

Lemma: const-poly-value
[n,f:Top].  (int_term_value(f;ipolynomial-term(const-poly(n))) n)

Definition: int_formulaco
int_formulaco() ==
  corec(X.lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
                     if lbl =a "le" then left:int_term() × int_term()
                     if lbl =a "eq" then left:int_term() × int_term()
                     if lbl =a "and" then left:X × X
                     if lbl =a "or" then left:X × X
                     if lbl =a "implies" then left:X × X
                     if lbl =a "not" then X
                     else Void
                     fi )

Lemma: int_formulaco_wf
int_formulaco() ∈ Type

Lemma: int_formulaco-ext
int_formulaco() ≡ lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
                             if lbl =a "le" then left:int_term() × int_term()
                             if lbl =a "eq" then left:int_term() × int_term()
                             if lbl =a "and" then left:int_formulaco() × int_formulaco()
                             if lbl =a "or" then left:int_formulaco() × int_formulaco()
                             if lbl =a "implies" then left:int_formulaco() × int_formulaco()
                             if lbl =a "not" then int_formulaco()
                             else Void

Definition: int_formulaco_size
int_formulaco_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "less" then 0
                   if lbl =a "le" then 0
                   if lbl =a "eq" then 0
                   if lbl =a "and" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "or" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "implies" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "not" then (size x)
                   else 0
                   fi )) 

Lemma: int_formulaco_size_wf
[p:int_formulaco()]. (int_formulaco_size(p) ∈ partial(ℕ))

Definition: int_formula
int_formula() ==  {p:int_formulaco()| (int_formulaco_size(p))↓

Lemma: int_formula_wf
int_formula() ∈ Type

Definition: int_formula_size
int_formula_size(p) ==
  fix((λsize,p. let lbl,x 
                in if lbl =a "less" then 0
                   if lbl =a "le" then 0
                   if lbl =a "eq" then 0
                   if lbl =a "and" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "or" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "implies" then (size (fst(x))) (size (snd(x)))
                   if lbl =a "not" then (size x)
                   else 0
                   fi )) 

Lemma: int_formula_size_wf
[p:int_formula()]. (int_formula_size(p) ∈ ℕ)

Lemma: int_formula-ext
int_formula() ≡ lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
                           if lbl =a "le" then left:int_term() × int_term()
                           if lbl =a "eq" then left:int_term() × int_term()
                           if lbl =a "and" then left:int_formula() × int_formula()
                           if lbl =a "or" then left:int_formula() × int_formula()
                           if lbl =a "implies" then left:int_formula() × int_formula()
                           if lbl =a "not" then int_formula()
                           else Void

Definition: intformless
(left "<right) ==  <"less", left, right>

Lemma: intformless_wf
[left,right:int_term()].  ((left "<right) ∈ int_formula())

Definition: intformle
left "≤right ==  <"le", left, right>

Lemma: intformle_wf
[left,right:int_term()].  (left "≤right ∈ int_formula())

Definition: intformeq
left "=" right ==  <"eq", left, right>

Lemma: intformeq_wf
[left,right:int_term()].  (left "=" right ∈ int_formula())

Definition: intformand
left "∧right ==  <"and", left, right>

Lemma: intformand_wf
[left,right:int_formula()].  (left "∧right ∈ int_formula())

Definition: intformor
left "or" right ==  <"or", left, right>

Lemma: intformor_wf
[left,right:int_formula()].  (left "or" right ∈ int_formula())

Definition: intformimplies
left "=>right ==  <"implies", left, right>

Lemma: intformimplies_wf
[left,right:int_formula()].  (left "=>right ∈ int_formula())

Definition: intformnot
"form ==  <"not", form>

Lemma: intformnot_wf
[form:int_formula()]. ("¬"form ∈ int_formula())

Definition: intformless?
intformless?(v) ==  fst(v) =a "less"

Lemma: intformless?_wf
[v:int_formula()]. (intformless?(v) ∈ 𝔹)

Definition: intformless-left
intformless-left(v) ==  fst(snd(v))

Lemma: intformless-left_wf
[v:int_formula()]. intformless-left(v) ∈ int_term() supposing ↑intformless?(v)

Definition: intformless-right
intformless-right(v) ==  snd(snd(v))

Lemma: intformless-right_wf
[v:int_formula()]. intformless-right(v) ∈ int_term() supposing ↑intformless?(v)

Definition: intformle?
intformle?(v) ==  fst(v) =a "le"

Lemma: intformle?_wf
[v:int_formula()]. (intformle?(v) ∈ 𝔹)

Definition: intformle-left
intformle-left(v) ==  fst(snd(v))

Lemma: intformle-left_wf
[v:int_formula()]. intformle-left(v) ∈ int_term() supposing ↑intformle?(v)

Definition: intformle-right
intformle-right(v) ==  snd(snd(v))

Lemma: intformle-right_wf
[v:int_formula()]. intformle-right(v) ∈ int_term() supposing ↑intformle?(v)

Definition: intformeq?
intformeq?(v) ==  fst(v) =a "eq"

Lemma: intformeq?_wf
[v:int_formula()]. (intformeq?(v) ∈ 𝔹)

Definition: intformeq-left
intformeq-left(v) ==  fst(snd(v))

Lemma: intformeq-left_wf
[v:int_formula()]. intformeq-left(v) ∈ int_term() supposing ↑intformeq?(v)

Definition: intformeq-right
intformeq-right(v) ==  snd(snd(v))

Lemma: intformeq-right_wf
[v:int_formula()]. intformeq-right(v) ∈ int_term() supposing ↑intformeq?(v)

Definition: intformand?
intformand?(v) ==  fst(v) =a "and"

Lemma: intformand?_wf
[v:int_formula()]. (intformand?(v) ∈ 𝔹)

Definition: intformand-left
intformand-left(v) ==  fst(snd(v))

Lemma: intformand-left_wf
[v:int_formula()]. intformand-left(v) ∈ int_formula() supposing ↑intformand?(v)

Definition: intformand-right
intformand-right(v) ==  snd(snd(v))

Lemma: intformand-right_wf
[v:int_formula()]. intformand-right(v) ∈ int_formula() supposing ↑intformand?(v)

Definition: intformor?
intformor?(v) ==  fst(v) =a "or"

Lemma: intformor?_wf
[v:int_formula()]. (intformor?(v) ∈ 𝔹)

Definition: intformor-left
intformor-left(v) ==  fst(snd(v))

Lemma: intformor-left_wf
[v:int_formula()]. intformor-left(v) ∈ int_formula() supposing ↑intformor?(v)

Definition: intformor-right
intformor-right(v) ==  snd(snd(v))

Lemma: intformor-right_wf
[v:int_formula()]. intformor-right(v) ∈ int_formula() supposing ↑intformor?(v)

Definition: intformimplies?
intformimplies?(v) ==  fst(v) =a "implies"

Lemma: intformimplies?_wf
[v:int_formula()]. (intformimplies?(v) ∈ 𝔹)

Definition: intformimplies-left
intformimplies-left(v) ==  fst(snd(v))

Lemma: intformimplies-left_wf
[v:int_formula()]. intformimplies-left(v) ∈ int_formula() supposing ↑intformimplies?(v)

Definition: intformimplies-right
intformimplies-right(v) ==  snd(snd(v))

Lemma: intformimplies-right_wf
[v:int_formula()]. intformimplies-right(v) ∈ int_formula() supposing ↑intformimplies?(v)

Definition: intformnot?
intformnot?(v) ==  fst(v) =a "not"

Lemma: intformnot?_wf
[v:int_formula()]. (intformnot?(v) ∈ 𝔹)

Definition: intformnot-form
intformnot-form(v) ==  snd(v)

Lemma: intformnot-form_wf
[v:int_formula()]. intformnot-form(v) ∈ int_formula() supposing ↑intformnot?(v)

Lemma: int_formula-induction
[P:int_formula() ⟶ ℙ]
  ((∀left,right:int_term().  P[(left "<right)])
   (∀left,right:int_term().  P[left "≤right])
   (∀left,right:int_term().  P[left "=" right])
   (∀left,right:int_formula().  (P[left]  P[right]  P[left "∧right]))
   (∀left,right:int_formula().  (P[left]  P[right]  P[left "or" right]))
   (∀left,right:int_formula().  (P[left]  P[right]  P[left "=>right]))
   (∀form:int_formula(). (P[form]  P["¬"form]))
   {∀v:int_formula(). P[v]})

Lemma: int_formula-definition
[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ].
  ((∀left,right:int_term().  {x:A| R[x;(left "<right)]} )
   (∀left,right:int_term().  {x:A| R[x;left "≤right]} )
   (∀left,right:int_term().  {x:A| R[x;left "=" right]} )
   (∀left,right:int_formula().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;left "∧right]} ))
   (∀left,right:int_formula().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;left "or" right]} ))
   (∀left,right:int_formula().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;left "=>right]} ))
   (∀form:int_formula(). ({x:A| R[x;form]}   {x:A| R[x;"¬"form]} ))
   {∀v:int_formula(). {x:A| R[x;v]} })

Definition: int_formula_ind
                intformless(left,right) less[left; right];
                intformle(left,right) le[left; right];
                intformeq(left,right) eq[left; right];
                intformand(left,right) rec1,rec2.and[left;
                intformor(left,right) rec3,rec4.or[left;
                intformimplies(left,right) rec5,rec6.implies[left;
                intformnot(form) rec7.not[form; rec7])  ==
  fix((λint_formula_ind,v. let lbl,v1 
                           in if lbl="less" then let left,v2 v1 in less[left; v2]
                              if lbl="le" then let left,v2 v1 in le[left; v2]
                              if lbl="eq" then let left,v2 v1 in eq[left; v2]
                              if lbl="and"
                                then let left,v2 v1 
                                     in and[left;
                                            int_formula_ind left;
                                            int_formula_ind v2]
                              if lbl="or"
                                then let left,v2 v1 
                                     in or[left;
                                           int_formula_ind left;
                                           int_formula_ind v2]
                              if lbl="implies"
                                then let left,v2 v1 
                                     in implies[left;
                                                int_formula_ind left;
                                                int_formula_ind v2]
                              if lbl="not" then not[v1; int_formula_ind v1]
                              else Ax
                              fi )) 

Lemma: int_formula_ind_wf
[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ]. ∀[v:int_formula()]. ∀[less:left:int_term()
                                                                    ⟶ right:int_term()
                                                                    ⟶ {x:A| R[x;(left "<right)]} ].
[le:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left "≤right]} ]. ∀[eq:left:int_term()
                                                                              ⟶ right:int_term()
                                                                              ⟶ {x:A| R[x;left "=" right]} ].
[and:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left "∧right]}\000C ].
[or:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left "or" right]}\000C ].
          ⟶ right:int_formula()
          ⟶ {x:A| R[x;left]} 
          ⟶ {x:A| R[x;right]} 
          ⟶ {x:A| R[x;left "=>right]} ]. ∀[not:form:int_formula() ⟶ {x:A| R[x;form]}  ⟶ {x:A| R[x;"¬"form]} ].
                   intformless(left,right) less[left;right];
                   intformle(left,right) le[left;right];
                   intformeq(left,right) eq[left;right];
                   intformand(left,right) rec1,rec2.and[left;right;rec1;rec2];
                   intformor(left,right) rec3,rec4.or[left;right;rec3;rec4];
                   intformimplies(left,right) rec5,rec6.implies[left;right;rec5;rec6];
                   intformnot(form) rec7.not[form;rec7])  ∈ {x:A| R[x;v]} )

Lemma: int_formula_ind_wf_simple
[A:Type]. ∀[v:int_formula()]. ∀[less,le,eq:left:int_term() ⟶ right:int_term() ⟶ A].
[and,or,implies:left:int_formula() ⟶ right:int_formula() ⟶ A ⟶ A ⟶ A]. ∀[not:form:int_formula() ⟶ A ⟶ A].
                   intformless(left,right) less[left;right];
                   intformle(left,right) le[left;right];
                   intformeq(left,right) eq[left;right];
                   intformand(left,right) rec1,rec2.and[left;right;rec1;rec2];
                   intformor(left,right) rec3,rec4.or[left;right;rec3;rec4];
                   intformimplies(left,right) rec5,rec6.implies[left;right;rec5;rec6];
                   intformnot(form) rec7.not[form;rec7])  ∈ A)

Definition: int_formula_prop
int_formula_prop(f;fmla) ==
                  a,b.int_term_value(f;a) < int_term_value(f;b);
                  a,b.int_term_value(f;a) ≤ int_term_value(f;b);
                  a,b.int_term_value(f;a) int_term_value(f;b) ∈ ℤ;
                  X,Y,PX,PY.PX ∧ PY;
                  X,Y,PX,PY.PX ∨ PY;
                  X,Y,PX,PY.PX  PY;

Lemma: int_formula_prop_wf
[f:ℤ ⟶ ℤ]. ∀[fmla:int_formula()].  (int_formula_prop(f;fmla) ∈ ℙ)

Lemma: istype-int_formula_prop
[f:ℤ ⟶ ℤ]. ∀[fmla:int_formula()].  istype(int_formula_prop(f;fmla))

Lemma: int_formula_prop_and_lemma
y,x,f:Top.  (int_formula_prop(f;x "∧y) int_formula_prop(f;x) ∧ int_formula_prop(f;y))

Lemma: int_formula_prop_or_lemma
y,x,f:Top.  (int_formula_prop(f;x "or" y) int_formula_prop(f;x) ∨ int_formula_prop(f;y))

Lemma: int_formual_prop_imp_lemma
y,x,f:Top.  (int_formula_prop(f;x "=>y) int_formula_prop(f;x)  int_formula_prop(f;y))

Lemma: int_formula_prop_not_lemma
x,f:Top.  (int_formula_prop(f;"¬"x) ~ ¬int_formula_prop(f;x))

Lemma: int_formula_prop_le_lemma
y,x,f:Top.  (int_formula_prop(f;x "≤y) int_term_value(f;x) ≤ int_term_value(f;y))

Lemma: int_formula_prop_less_lemma
y,x,f:Top.  (int_formula_prop(f;(x "<y)) int_term_value(f;x) < int_term_value(f;y))

Lemma: int_formula_prop_eq_lemma
y,x,f:Top.  (int_formula_prop(f;x "=" y) int_term_value(f;x) int_term_value(f;y) ∈ ℤ)

Lemma: int_formula-subtype-base
int_formula() ⊆Base

Definition: satisfiable_int_formula
satisfiable_int_formula(fmla) ==  ∃f:ℤ ⟶ ℤint_formula_prop(f;fmla)

Lemma: satisfiable_int_formula_wf
[fmla:int_formula()]. (satisfiable_int_formula(fmla) ∈ ℙ)

Definition: polynomial-constraints
polynomial-constraints() ==  iPolynomial() List × (iPolynomial() List)

Lemma: polynomial-constraints_wf
polynomial-constraints() ∈ Type

Definition: satisfies-poly-constraints
satisfies-poly-constraints(f;X) ==
  let eqs,ineqs 
  in (∀p∈eqs.int_term_value(f;ipolynomial-term(p)) 0 ∈ ℤ) ∧ (∀p∈ineqs.0 ≤ int_term_value(f;ipolynomial-term(p)))

Lemma: satisfies-poly-constraints_wf
[f:ℤ ⟶ ℤ]. ∀[X:polynomial-constraints()].  (satisfies-poly-constraints(f;X) ∈ ℙ)

Definition: satisfiable_polynomial_constraints
satisfiable_polynomial_constraints(X) ==  ∃f:ℤ ⟶ ℤsatisfies-poly-constraints(f;X)

Lemma: satisfiable_polynomial_constraints_wf
[X:polynomial-constraints()]. (satisfiable_polynomial_constraints(X) ∈ ℙ)

Definition: combine-pcs
combine-pcs(X;Y) ==  let eqsX,ineqsX in let eqsY,ineqsY in <eqsX eqsY, ineqsX ineqsY>

Lemma: combine-pcs_wf
[X,Y:polynomial-constraints()].  (combine-pcs(X;Y) ∈ polynomial-constraints())

Lemma: satisfies-combine-pcs
f:ℤ ⟶ ℤ. ∀A,B:polynomial-constraints().
  (satisfies-poly-constraints(f;combine-pcs(A;B)) ⇐⇒ satisfies-poly-constraints(f;A) ∧ satisfies-poly-constraints(f;B))

Definition: and-poly-constraints
and-poly-constraints(Xs;Ys) ==
  accumulate (with value sofar and list item Y):
   accumulate (with value sofar' and list item X):
    [combine-pcs(X;Y) sofar']
   over list:
   with starting value:
  over list:
  with starting value:

Lemma: and-poly-constraints_wf
[Xs,Ys:polynomial-constraints() List].  (and-poly-constraints(Xs;Ys) ∈ polynomial-constraints() List)

Lemma: member-and-poly-constraints
L1,L2:polynomial-constraints() List. ∀X:polynomial-constraints().
  ((X ∈ and-poly-constraints(L1;L2)) ⇐⇒ (∃A∈L1. (∃B∈L2. combine-pcs(A;B) ∈ polynomial-constraints())))

Lemma: satisfies-and-poly-constraints
f:ℤ ⟶ ℤ. ∀L2,L1:polynomial-constraints() List.
  ((∃X∈L1. satisfies-poly-constraints(f;X)) ∧ (∃X∈L2. satisfies-poly-constraints(f;X))
  ⇐⇒ (∃X∈and-poly-constraints(L1;L2). satisfies-poly-constraints(f;X)))

Definition: negate-poly-constraint
negate-poly-constraint(X) ==
  let eqs,ineqs 
  in accumulate (with value pcs and list item e):
      [<[], [minus-poly(add-ipoly(e;const-poly(1)))]>[<[], [add-ipoly(e;const-poly(-1))]> pcs]]
     over list:
     with starting value:
      map(λineq.<[], [minus-poly(add-ipoly(ineq;const-poly(1)))]>;ineqs))

Lemma: negate-poly-constraint_wf
[X:polynomial-constraints()]. (negate-poly-constraint(X) ∈ polynomial-constraints() List)

Lemma: satisfies-negate-poly-constraint
X:polynomial-constraints(). ∀f:ℤ ⟶ ℤ.
  ((∃Z∈negate-poly-constraint(X). satisfies-poly-constraints(f;Z)) ⇐⇒ ¬satisfies-poly-constraints(f;X))

Definition: negate-poly-constraints
negate-poly-constraints(Xs) ==
  if null(Xs)
  then [<[], []>]
  else let x,more Xs 
       in accumulate (with value sofar and list item X):
          over list:
          with starting value:

Lemma: negate-poly-constraints_wf
[Xs:polynomial-constraints() List]. (negate-poly-constraints(Xs) ∈ polynomial-constraints() List)

Lemma: satisfies-negate-poly-constraints
f:ℤ ⟶ ℤ. ∀L:polynomial-constraints() List.
  ((∀X∈L.¬satisfies-poly-constraints(f;X)) ⇐⇒ (∃X∈negate-poly-constraints(L). satisfies-poly-constraints(f;X)))

Definition: int_formula_dnf
int_formula_dnf(fmla) ==
                  a,b.[<[], [int_term_to_ipoly(b (-) (+) "1")]>];
                  a,b.[<[], [int_term_to_ipoly(b (-) a)]>];
                  a,b.[<[int_term_to_ipoly(b (-) a)], []>];
                  X,Y,nfX,nfY.nfX nfY;
                  X,Y,nfX,nfY.negate-poly-constraints(nfX) nfY;

Lemma: int_formula_dnf_wf
[fmla:int_formula()]. (int_formula_dnf(fmla) ∈ polynomial-constraints() List)

Lemma: satisfies_int_formula_dnf
fmla:int_formula(). ∀f:ℤ ⟶ ℤ.
  (int_formula_prop(f;fmla) ⇐⇒ (∃X∈int_formula_dnf(fmla). satisfies-poly-constraints(f;X)))

Lemma: satisfiable_int_formula_dnf
  (satisfiable_int_formula(fmla) ⇐⇒ (∃X∈int_formula_dnf(fmla). satisfiable_polynomial_constraints(X)))

Definition: polynomial-mon-vars
polynomial-mon-vars(init;p) ==
  accumulate (with value vss and list item m):
   let c,vs 
   in insert(vs;vss)
  over list:
  with starting value:

Lemma: polynomial-mon-vars_wf
[init:ℤ List List]. ∀[p:(Top × (ℤ List)) List].  (polynomial-mon-vars(init;p) ∈ ℤ List List)

Lemma: member-polynomial-mon-vars
p:iMonomial() List. ∀L:ℤ List List. ∀vs:ℤ List.
  ((vs ∈ polynomial-mon-vars(L;p)) ⇐⇒ (vs ∈ L) ∨ (∃m∈p. vs (snd(m)) ∈ (ℤ List)))

Lemma: no_repeats-polynomial-mon-vars
p:iMonomial() List. ∀L:ℤ List List.  (no_repeats(ℤ List;L)  no_repeats(ℤ List;polynomial-mon-vars(L;p)))

Definition: pcs-mon-vars
pcs-mon-vars(X) ==
  let eqs,ineqs 
  in accumulate (with value vs and list item p):
     over list:
     with starting value:
      accumulate (with value vs and list item p):
      over list:
      with starting value:

Lemma: pcs-mon-vars_wf
[X:polynomial-constraints()]. (pcs-mon-vars(X) ∈ ℤ List List)

Lemma: member-pcs-mon-vars
X:polynomial-constraints(). ∀vs:ℤ List.
  ((vs ∈ pcs-mon-vars(X))
  ⇐⇒ (vs [] ∈ (ℤ List))
      ∨ (∃p∈fst(X). (∃m∈p. vs (snd(m)) ∈ (ℤ List)))
      ∨ (∃p∈snd(X). (∃m∈p. vs (snd(m)) ∈ (ℤ List))))

Lemma: no_repeats-pcs-mon-vars
X:polynomial-constraints(). no_repeats(ℤ List;pcs-mon-vars(X))

Lemma: hd-rev-pcs-mon-vars
X:polynomial-constraints(). (0 < ||rev(pcs-mon-vars(X))|| ∧ (hd(rev(pcs-mon-vars(X))) [] ∈ (ℤ List)))

Definition: poly-coeff-of
poly-coeff-of(vs;p) ==
  rec-case(p) of
  [] => 0
  m::ps2 =>
   r.let c,ws 
     in if ws ≤_lex vs then if vs ≤_lex ws then else fi  else fi 

Lemma: poly-coeff-of_wf
[vs:ℤ List]. ∀[p:iPolynomial()].  (poly-coeff-of(vs;p) ∈ ℤ)

Definition: linearization
linearization(p;L) ==  map(λvs.poly-coeff-of(vs;p);L)

Lemma: linearization_wf
[p:iPolynomial()]. ∀[L:ℤ List List].  (linearization(p;L) ∈ {cs:ℤ List| ||cs|| ||L|| ∈ ℤ)

Lemma: linearization-value
[L:ℤ List List]. ∀[p:iPolynomial()].
  ∀f:ℤ ⟶ ℤ
    linearization(p;L) ⋅ map(λvs.accumulate (with value and list item v):
                                    (f v)
                                   over list:
                                   with starting value:
    ∈ ℤ
  supposing (∀m∈p.(snd(m) ∈ L)) ∧ no_repeats(ℤ List;L)

Definition: pcs-to-integer-problem
pcs-to-integer-problem(X) ==
  eval rev(pcs-mon-vars(X)) in
  let polyeqs,polyineqs 
  in eval eqs evalall(eager-map(λp.linearization(p;L);polyeqs)) in
     eval ineqs evalall(eager-map(λp.linearization(p;L);polyineqs)) in
       <eqs, ineqs>

Lemma: pcs-to-integer-problem_wf
  (pcs-to-integer-problem(X) ∈ ⋃n:ℕ.({L:ℤ List| ||L|| (n 1) ∈ ℤ}  List × ({L:ℤ List| ||L|| (n 1) ∈ ℤ}  List)))

Definition: satisfies-integer-problem
satisfies-integer-problem(eqs;ineqs;xs) ==  (∀as∈eqs.xs ⋅ as =0) ∧ (∀bs∈ineqs.xs ⋅ bs ≥0)

Lemma: satisfies-integer-problem_wf
[eqs,ineqs:ℤ List List]. ∀[xs:ℤ List].  (satisfies-integer-problem(eqs;ineqs;xs) ∈ ℙ)

Definition: satisfiable-integer-problem
satisfiable(eqs;ineqs) ==  ∃xs:ℤ List. satisfies-integer-problem(eqs;ineqs;xs)

Lemma: satisfiable-integer-problem_wf
[eqs,ineqs:ℤ List List].  (satisfiable(eqs;ineqs) ∈ ℙ)

Lemma: satisfiable-pcs-to-integer-problem
  (satisfiable_polynomial_constraints(X)  satisfiable(fst(pcs-to-integer-problem(X));snd(pcs-to-integer-problem(X))))

Lemma: satisfies-integer-problem-length
[eqs,ineqs:ℤ List List]. ∀[xs:ℤ List].
  {(∀e∈eqs.||e|| ||xs|| ∈ ℤ) ∧ (∀e∈ineqs.||e|| ||xs|| ∈ ℤ)} supposing satisfies-integer-problem(eqs;ineqs;xs)

Definition: exact-eq-constraint
exact-eq-constraint(eqs;i;j) ==  |eqs[i][j]| 1 ∈ ℤ

Lemma: exact-eq-constraint_wf
[eqs:ℤ List List]. ∀[i:ℕ||eqs||]. ∀[j:ℕ||eqs[i]||].  (exact-eq-constraint(eqs;i;j) ∈ ℙ)

Lemma: exact-eq-constraint-implies
[eqs:ℤ List List]. ∀[i:ℕ||eqs||]. ∀[j:ℕ||eqs[i]||].
  ∀ineqs:ℤ List List. ∀xs:ℤ List.
     (xs[j] if (eqs[i][j] =z 1) then -1 eqs[i]\j ⋅ xs\j else eqs[i]\j ⋅ xs\j fi  ∈ ℤ)) 
  supposing exact-eq-constraint(eqs;i;j)

Definition: exact-reduce-constraints
exact-reduce-constraints(w;j;L) ==  evalall(map(λv.-(w[j] v[j]) w\j v\j;L))

Lemma: exact-reduce-constraints_wf
[w:ℤ List]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| ||w|| ∈ ℤ}  List].
  (exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| (||w|| 1) ∈ ℤ}  List)

Lemma: exact-reduce-constraints-sqequal
[w:ℤ List]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| ||w|| ∈ ℤ}  List].
  (exact-reduce-constraints(w;j;L) map(λv.-(w[j] v[j]) w\j v\j;L))

Lemma: satisfiable-exact-reduce-constraints
eqs:ℤ List List. ∀i:ℕ||eqs||. ∀j:ℕ+||eqs[i]||.
  ∀ineqs:ℤ List List
  supposing exact-eq-constraint(eqs;i;j)

Lemma: satisfiable-elim-eq-constraints
eqs,ineqs:ℤ List List. ∀xs:ℤ List.
   satisfies-integer-problem([];(eager-map(λeq.eager-map(λx.(-x);eq);eqs) eqs) ineqs;xs))

Definition: gcd-reduce-eq-constraints
Each equality constraint is list [c,a1,a2,...] and represents the
constraint  a1*v1 a2*v2 ....  (on variables v1, v2, ...).
If gcd(a1,a2,...) is greater than 1, then if is not divisible by g
then the constraint is unsatisfiable.
Otherwise we can divide and all the a1,a2,... by and preserve

gcd-reduce-eq-constraints(sat;LL) ==
  accumulate_abort(L,Ls.let h,t 
                        in if Ax then if h=0 then inl [L Ls] else (inr ⋅ )
                           otherwise eval |gcd-list(t)| in
                                     if (1) < (g)
                                        then if rem g=0
                                             then eval L' eager-map(λx.(x ÷ g);L) in
                                                  inl [L' Ls]
                                             else (inr ⋅ )
                                        else (inl [L Ls]);inl sat;LL)

Lemma: gcd-reduce-eq-constraints_wf
[LL,sat:ℤ List+ List].  (gcd-reduce-eq-constraints(sat;LL) ∈ ℤ List+ List?)

Lemma: member-gcd-reduce-constraints
n:ℕ+. ∀eqs,sat:{L:ℤ List| ||L|| n ∈ ℤ}  List. ∀cc:{L:ℤ List| ||L|| n ∈ ℤ.
  ((↑isl(gcd-reduce-eq-constraints(sat;eqs)))  (cc ∈ sat)  (cc ∈ outl(gcd-reduce-eq-constraints(sat;eqs))))

Lemma: satisfies-gcd-reduce-eq-constraints
[n:ℕ+]. ∀[eqs,sat:{L:ℤ List| ||L|| n ∈ ℤ}  List]. ∀[xs:{L:ℤ List| ||L|| n ∈ ℤ].
  uiff((∀as∈eqs.xs ⋅ as =0);(↑isl(gcd-reduce-eq-constraints(sat;eqs)))
  ∧ (∀as∈outl(gcd-reduce-eq-constraints(sat;eqs)).xs ⋅ as =0)) 
  supposing (∀as∈sat.xs ⋅ as =0) ∧ 0 < ||xs|| ∧ (hd(xs) 1 ∈ ℤ)

Definition: gcd-reduce-ineq-constraints
Each inequality constraint is list [c,a1,a2,...] and represents the
constraint  a1*v1 a2*v2 ....  >(on variables v1, v2, ...).
If gcd(a1,a2,...) is greater than then we
divide all the a1,a2,... by and replace by the "floor" of ⌜c ÷ g⌝.
This preserves the satisfiability of the inequality.⋅

gcd-reduce-ineq-constraints(sat;LL) ==
  accumulate_abort(L,Ls.let h,t 
                        in if Ax then if (h) < (0)  then inr ⋅   else (inl [L Ls])
                           otherwise eval |gcd-list(t)| in
                                     if (1) < (g)
                                        then eval h' h ÷↓ in
                                             eval t' eager-map(λx.(x ÷ g);t) in
                                               inl [[h' t'] Ls]
                                        else (inl [L Ls]);inl sat;LL)

Lemma: gcd-reduce-ineq-constraints_wf
[LL,sat:ℤ List+ List].  (gcd-reduce-ineq-constraints(sat;LL) ∈ ℤ List+ List?)

Lemma: member-gcd-reduce-ineq-constraints
n:ℕ+. ∀ineqs,sat:{L:ℤ List| ||L|| n ∈ ℤ}  List. ∀cc:{L:ℤ List| ||L|| n ∈ ℤ.
  ((↑isl(gcd-reduce-ineq-constraints(sat;ineqs)))  (cc ∈ sat)  (cc ∈ outl(gcd-reduce-ineq-constraints(sat;ineqs))))

Lemma: satisfies-gcd-reduce-ineq-constraints
[n:ℕ+]. ∀[ineqs,sat:{L:ℤ List| ||L|| n ∈ ℤ}  List]. ∀[xs:{L:ℤ List| ||L|| n ∈ ℤ].
  uiff((∀as∈ineqs.xs ⋅ as ≥0);(↑isl(gcd-reduce-ineq-constraints(sat;ineqs)))
  ∧ (∀as∈outl(gcd-reduce-ineq-constraints(sat;ineqs)).xs ⋅ as ≥0)) 
  supposing (∀as∈sat.xs ⋅ as ≥0) ∧ 0 < ||xs|| ∧ (hd(xs) 1 ∈ ℤ)

Definition: shadow-inequalities
For the given index, i, divide the inequality constraints into ,
those where the i-th coefficient is >0, and those where it is <
(and ignore -- hence delete -- those where the i-th coefficient is =0)

For each as in the first part and each bs in the second part, form the 
"shadow-vec". The list of all of these is the new set of constraints
in which the i-th variable has been eliminated.

In the worst case, constraints in k+1 variables can result in
  (N/2)*(N/2) N^2/4 constraints in variables. But this does not seem
to happen in practice for typical theorem proving applications.⋅

shadow-inequalities(i;ineqs) ==
  eval evalall(map(λL.L\i;filter(λL.(L[i] =z 0);ineqs))) in
  eager-append(eager-product-map(λas,bs. shadow-vec(i;as;bs);filter(λL.0 <L[i];ineqs);filter(λL.L[i] <0;ineqs));Z)

Lemma: shadow-inequalities_wf
[n:ℕ]. ∀[ineqs:{L:ℤ List| ||L|| n ∈ ℤ}  List]. ∀[i:ℕn].
  (shadow-inequalities(i;ineqs) ∈ {L:ℤ List| ||L|| (n 1) ∈ ℤ}  List)

Lemma: satisfies-shadow-inequalities
[n:ℕ]. ∀[ineqs:{L:ℤ List| ||L|| n ∈ ℤ}  List]. ∀[i:ℕ+n]. ∀[xs:ℤ List].
  (∀as∈shadow-inequalities(i;ineqs).xs\i ⋅ as ≥0) supposing (∀as∈ineqs.xs ⋅ as ≥0)

Definition: max_tl_coeffs
max_tl_coeffs(ineqs) ==  eager-accum(L1,ineq.map2(λx,y. imax(x;|y|);L1;tl(ineq));map(λx.|x|;tl(hd(ineqs)));tl(ineqs))

Lemma: max_tl_coeffs_wf
[n:ℕ+]. ∀[ineqs:{L:ℤ List| ||L|| n ∈ ℤ}  List+].  (max_tl_coeffs(ineqs) ∈ {L:ℤ List| ||L|| (n 1) ∈ ℤ)

Definition: shadow_inequalities
Find the variable whose maximum coefficient (in any of the constraints) is
the least, and eliminate that variable by computing its
"shadow inequalities".  This the the heuristic used by Bill Pugh in the 
original version of the omega test.⋅

shadow_inequalities(ineqs) ==
  if ineqs Ax then ineqs otherwise eval index-of-min(max_tl_coeffs(ineqs)) in

Lemma: shadow_inequalities_wf
[n:{2...}]. ∀[ineqs:{L:ℤ List| ||L|| n ∈ ℤ}  List].  (shadow_inequalities(ineqs) ∈ {L:ℤ List| ||L|| (n 1) ∈ ℤ}  L\000Cist)

Lemma: satisfies-shadow_inequalities
  ∀ineqs:{L:ℤ List| ||L|| n ∈ ℤ}  List
    ((∃xs:ℤ List. (∀as∈ineqs.xs ⋅ as ≥0))  (∃xs:ℤ List. (∀as∈shadow_inequalities(ineqs).xs ⋅ as ≥0)))

Definition: test-exact-eq-constraint
test-exact-eq-constraint(L) ==
  rec-case(L) of
  [] => inr ⋅ 
  a::as =>
   r.if (|a| =z 1) then inl else case of inl(n) => inl (n 1) inr(x) => inr x  fi 

Lemma: test-exact-eq-constraint_wf
[L:ℤ List]. (test-exact-eq-constraint(L) ∈ ∃i:ℕ||L|| [(|L[i]| 1 ∈ ℤ)]?)

Definition: find-exact-eq-constraint
find-exact-eq-constraint(L) ==
  let a,as 
  in case test-exact-eq-constraint(as) of inl(n) => inl <L, 1> inr(x) => inr 

Lemma: find-exact-eq-constraint_wf
[L:ℤ List]. find-exact-eq-constraint(L) ∈ x:{x:ℤ List| L ∈ (ℤ List)}  × {i:ℕ+||L||| |L[i]| 1 ∈ ℤsupposing 0 <\000C ||L||

Definition: int-constraint-problem
IntConstraints ==  ⋃n:ℕ.({L:ℤ List| ||L|| (n 1) ∈ ℤ}  List × ({L:ℤ List| ||L|| (n 1) ∈ ℤ}  List))?

Lemma: int-constraint-problem_wf
IntConstraints ∈ Type

Definition: satisfies-int-constraint-problem
xs |= ==  case of inl(q) => let eqs,ineqs in (∀as∈eqs.xs ⋅ as =0) ∧ (∀bs∈ineqs.xs ⋅ bs ≥0) inr(_) => False

Lemma: satisfies-int-constraint-problem_wf
[p:IntConstraints]. ∀[xs:ℤ List].  (xs |= p ∈ ℙ)

Definition: unsat-int-problem
unsat(p) ==  ∀xs:ℤ List. xs |= p)

Lemma: unsat-int-problem_wf
[p:IntConstraints]. (unsat(p) ∈ ℙ)

Definition: int-problem-dimension
If the integer problem is known to be unsatisfiable (the inr case) then 
it has dimension 0. Otherwise, all the constraints are lists of the 
same length, [c,a1,a2,...] representing the linear form 
 c+ a1*v1 a2*v2 ....,  so the dimension is the length of (any of) these
lists decremented by 1.⋅

dim(p) ==
  case p
   of inl(q) =>
   let eqs,ineqs 
   in if eqs Ax then if ineqs Ax then otherwise ||hd(ineqs)|| otherwise ||hd(eqs)|| 1
   inr(_) =>

Lemma: int-problem-dimension_wf
[p:IntConstraints]. (dim(p) ∈ ℕ)

Definition: num-eq-constraints
num-eq-constraints(p) ==  case of inl(q) => ||fst(q)|| inr(_) => 0

Lemma: num-eq-constraints_wf
[p:IntConstraints]. (num-eq-constraints(p) ∈ ℕ)

Definition: rep_int_constraint_step
Keep applying as long as the dimension of the "integer problem" is
greater than 0.⋅

rep_int_constraint_step(f;p)==r if (0) < (dim(p))  then let p' ⟵ in rep_int_constraint_step(f;p')  else p

Lemma: rep_int_constraint_step_wf
[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
  rep_int_constraint_step(f;p) ∈ {p:IntConstraints| dim(p) 0 ∈ ℤ}  
  supposing ∀p:IntConstraints
              (0 < dim(p)
               (dim(f p) < dim(p) ∨ ((dim(f p) dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p))))

Lemma: isr-rep_int_constraint_step
[f:IntConstraints ⟶ IntConstraints]. ∀[p:IntConstraints].
  (unsat(p)) supposing 
     ((↑isr(rep_int_constraint_step(f;p))) and 
         (0 < dim(p)
          (dim(f p) < dim(p) ∨ ((dim(f p) dim(p) ∈ ℤ) ∧ num-eq-constraints(f p) < num-eq-constraints(p)))))
     ∧ (∀p:IntConstraints. (unsat(f p)  unsat(p)))))

Lemma: gcd-reduce-ineq-constraints_wf2
[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| (n 1) ∈ ℤ}  List].
  (gcd-reduce-ineq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| (n 1) ∈ ℤ}  List?)

Lemma: gcd-reduce-eq-constraints_wf2
[n:ℕ]. ∀[LL,sat:{L:ℤ List| ||L|| (n 1) ∈ ℤ}  List].
  (gcd-reduce-eq-constraints(sat;LL) ∈ {L:ℤ List| ||L|| (n 1) ∈ ℤ}  List?)

Lemma: exact-reduce-constraints_wf2
[n:ℕ]. ∀[w:{l:ℤ List| ||l|| (n 1) ∈ ℤ]. ∀[j:ℕ||w||]. ∀[L:{l:ℤ List| ||l|| (n 1) ∈ ℤ}  List].
  (exact-reduce-constraints(w;j;L) ∈ {l:ℤ List| ||l|| ((n 1) 1) ∈ ℤ}  List)

Definition: omega_step
The "omega step" first searches for an "exact" equality constraint (one where
the coefficient of variable is or -1). In that case, the constraint can
be solved exactly for that variable, and the variable can be eliminated.
(If that happens, we then run the "gcd-reduce" operations on the resulting

If there is no exact equality constraint, but there are still equality
constraints, then we convert each remaining equality constraints into
two inequality constraints.  (Bill Pugh has better procedure for
dealing with in-exact equality constraints, but we haven't implemented it.)

If there are no more equality constraints, then omega computes the
"shadow inequalities" for chosen variable -- which eliminates that variable. 

omega_step(p) ==
  if (dim(p)) < (1)
     then p
     else case p
           of inl(q) =>
           let eqs,ineqs 
           in case first-success(λL.find-exact-eq-constraint(L);eqs)
               of inl(tr) =>
               let i,wj tr 
               in let w,j wj 
                  in case gcd-reduce-eq-constraints([];exact-reduce-constraints(w;j;eqs))
                      of inl(eqs') =>
                      case gcd-reduce-ineq-constraints([];exact-reduce-constraints(w;j;ineqs))
                       of inl(ineqs') =>
                       inl <eqs', ineqs'>
                       inr(x) =>
                      inr(x) =>
               inr(_) =>
               if null(eqs)
               then case gcd-reduce-ineq-constraints([];shadow_inequalities(ineqs))
                     of inl(ineqs') =>
                     inl <[], ineqs'>
                     inr(x) =>
               else inl <[], (eager-map(λeq.eager-map(λx.(-x);eq);eqs) eqs) ineqs>
           inr(_) =>

Lemma: omega_step_wf
[p:IntConstraints]. (omega_step(p) ∈ IntConstraints)

Lemma: omega_step_measure
  (0 < dim(p)
   (dim((λp.omega_step(p)) p) < dim(p)
     ∨ ((dim((λp.omega_step(p)) p) dim(p) ∈ ℤ) ∧ num-eq-constraints((λp.omega_step(p)) p) < num-eq-constraints(p))))

Lemma: unsat-omega_step
p:IntConstraints. (unsat(omega_step(p))  unsat(p))

Definition: omega_start
To create starting state of omega, we "gcd-reduce" the constraints.
This can sometimes detect that the equality constraints are unsatisfiable.⋅

omega_start(eqs;ineqs) ==
  case gcd-reduce-eq-constraints([];eqs)
   of inl(eqs') =>
   case gcd-reduce-ineq-constraints([];ineqs) of inl(ineqs') => inl <eqs', ineqs'> inr(x) => inr 
   inr(x) =>

Lemma: omega_start_wf
[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| (n 1) ∈ ℤ}  List].  (omega_start(eqs;ineqs) ∈ IntConstraints)

Lemma: unsat-omega_start
n:ℕ. ∀eqs,ineqs:{L:ℤ List| ||L|| (n 1) ∈ ℤ}  List.  (unsat(omega_start(eqs;ineqs))  satisfiable(eqs;ineqs)))

Definition: omega
omega works on an "integer problem" that is set of equality constraints
and set of inequality constraints. It start by normalizing the constraints.
Then it repeats the "omega_step". On each step, either the number of 
equality constraints decreases, or the dimension of the problem (the number
of variables) decreases. Thus the algorithm terminates.

Each step preserves satisfiablity of the constraints, meaning that if
the resulting problem is unsatisfiable then the original problem is
unsatisfiable. Because we have not implemented Bill Pugh's "dark shadow"
test, the reverse is not true in general (the reduced problem could be
satisfiable even though the original problem was unsatisfiable).⋅

omega(eqs;ineqs) ==  let s ⟵ omega_start(eqs;ineqs) in rep_int_constraint_step(λp.omega_step(p);s)

Lemma: omega_wf
[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| (n 1) ∈ ℤ}  List].  (omega(eqs;ineqs) ∈ {p:IntConstraints| dim(p) 0 ∈ ℤ)

Lemma: isr-omega
[n:ℕ]. ∀[eqs,ineqs:{L:ℤ List| ||L|| (n 1) ∈ ℤ}  List].  ¬satisfiable(eqs;ineqs) supposing ↑isr(omega(eqs;ineqs))

Definition: full-omega
full-omega works on "integer formulas". It first puts the formula
into disjunctive-normal-form where each disjunct is collection
of "polynomial constraints" (a polynomial in the "atoms" of the formula
which is either =0 or >0).

Each set of polynomial constraints is "linearized" to (linear) 
"integer problem", set of linear forms =0 or >0.

omega is run on each of these problems, and if all the results are ff
then the formula is unsatisfiable. If any of the results are tt
then the formlua might be satisfiable, but is not guaranteed to be.
That is because we have not implemented Bill Pugh's "dark shadow" test.

However, for theorem proving, "semi decision" that can guarantees that
formula is unsatisfiable seems to be good enough.⋅

full-omega(fmla) ==
  eval dnf evalall(int_formula_dnf(fmla)) in
  ∨blet eqs,ineqs pcs-to-integer-problem(pc) 
    in case omega(eqs;ineqs) of inl(x) => tt inr(_) => ff;ff;dnf)

Lemma: full-omega_wf
[fmla:int_formula()]. (full-omega(fmla) ∈ {b:𝔹ff  satisfiable_int_formula(fmla))} )

Lemma: satisfiable-full-omega-tt
[fmla:int_formula()]. ↑isl(full-omega(fmla)) supposing satisfiable_int_formula(fmla)

Lemma: full-omega-unsat
[fmla:int_formula()]. ¬satisfiable_int_formula(fmla) supposing inr Ax  ≤ full-omega(fmla)

Lemma: test-omega
x,y,z:ℤ.  ((1 ≤ ((2 x) (2 y)))  ((2 x) ≤ ((2 y) 1))  (2 ≤ (3 y)))

Lemma: test-omega2
  ((((p0 q1) (q0 r1) (r0 p1)) (p1 q0) (q1 r0) (r1 p0))
  ((((t0 q1) (q0 r1) (r0 t1)) (t1 q0) (q1 r0) (r1 t0))
    (((p0 t1) (t0 r1) (r0 p1)) (p1 t0) (t1 r0) (r1 p0))
    (((p0 q1) (q0 t1) (t0 p1)) (p1 q0) (q1 t0) (t1 p0)))
  ∈ ℤ)

Lemma: test-omega-auto-split
n:ℤ(if 2 <then if 1 <then else fi  if n ≤then else fi  if 2 <then else fi )

Definition: ml-int-vec-mul
ml-int-vec-mul(a;as) ==  ml-map(λx.(a x);as)

Lemma: ml-int-vec-mul_wf
[a:ℤ]. ∀[as:ℤ List].  (ml-int-vec-mul(a;as) ∈ ℤ List)

Lemma: ml-int-vec-mul-sq
[a:ℤ]. ∀[as:ℤ List].  (ml-int-vec-mul(a;as) as)

Definition: ml-int-vec-add
ml-int-vec-add(as;bs) ==
  fix((λivadd,as,bs. if null(as) ∨bnull(bs)
                    then []
                    else let a.as2 as 
                         in let b.bs2 bs 
                            in [a ivadd(as2)(bs2)]
                    fi ))(as)(bs)

Lemma: ml-int-vec-add-sq
[as,bs:ℤ List].  (ml-int-vec-add(as;bs) as bs)

Lemma: ml-int-vec-add_wf
[as,bs:ℤ List].  (ml-int-vec-add(as;bs) ∈ ℤ List)

Definition: ml-list-delete
ml-list-delete(as;i) ==
  fix((λlistdel,as,i. if null(as)
                     then []
                     else let a.more as 
                          in if i <then more else [a listdel(more)(i 1)] fi 
                     fi ))(as)(i)

Lemma: ml-list-delete-sq
[T:Type]. ∀[L:T List]. ∀[i:ℤ].  (ml-list-delete(L;i) L\i) supposing valueall-type(T)

Lemma: ml-list-delete_wf
[T:Type]. ∀[L:T List]. ∀[i:ℤ].  (ml-list-delete(L;i) ∈ List) supposing valueall-type(T)

Definition: ml-accum-abort
ml-accum-abort(f;sofar;L) ==
  fix((λacca,f,sofar,L. if null(L) ∨bisr(sofar) then sofar else let x.y in acca(f)(f(x)(outl(sofar)))(y) fi ))(f)(so\000Cfar)(L)

Lemma: ml-accum-abort-sq
[A,B:Type]. ∀[F:A ⟶ B ⟶ (B?)].
  ∀[L:A List]. ∀[s:B?].  (ml-accum-abort(F;s;L) accumulate_abort(x,sofar.F sofar;s;L)) 
  supposing valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B

Lemma: ml-accum-abort_wf
[A,B:Type]. ∀[s:B?]. ∀[F:A ⟶ B ⟶ (B?)]. ∀[L:A List].
  ml-accum-abort(F;s;L) ∈ B? supposing valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B

Definition: ml-gcd-reduce-eq-constraints
ml-gcd-reduce-eq-constraints(sat;LL) ==
  ml-accum-abort(λL,Ls. let h.t 
                        in if null(t)
                           then if (h =z 0) then inl [L Ls] else inr ⋅  fi 
                           else let ml-absval(ml-gcd-list(t)) in
                                    if 1 <g
                                    then if (h rem =z 0) then inl [ml-map(λx.(x ÷ g);L) Ls] else inr ⋅  fi 
                                    else inl [L Ls]
                           fi ;inl sat;LL)

Definition: ml-shadow-vec
ml-shadow-vec(i;as;bs) ==

Home Index