---

Step * of Lemma member-gcd-reduce-ineq-constraints

No Annotations
∀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))))
BY
{ (InductionOnList
   THEN Unfold `gcd-reduce-ineq-constraints` 0
   THEN (RWW "accumulate_abort_cons_lemma" 0 THENA Auto)
   THEN Reduce 0
   THEN Try (Complete (Auto))) }

1
1. n : ℕ+
2. u : {L:ℤ List| ||L|| = n ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = n ∈ ℤ}  List
4. ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ}  List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
     ((↑isl(gcd-reduce-ineq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-ineq-constraints(sat;v))))
⊢ ∀sat:{L:ℤ List| ||L|| = n ∈ ℤ}  List. ∀cc:{L:ℤ List| ||L|| = n ∈ ℤ} .
    ((↑isl(let s' ⟵ let h,t = u 
                     in if t = Ax then if (h) < (0)  then inr ⋅   else (inl [u / sat])
                        otherwise eval g = |gcd-list(t)| in
                                  if (1) < (g)
                                     then eval h' = h ÷↓ g in
                                          eval t' = eager-map(λx.(x ÷ g);t) in
                                            inl [[h' / t'] / sat]
                                     else (inl [u / sat])
           in accumulate_abort(L,Ls.let h,t = L 
                                    in if t = Ax then if (h) < (0)  then inr ⋅   else (inl [L / Ls])
                                       otherwise eval g = |gcd-list(t)| in
                                                 if (1) < (g)
                                                    then eval h' = h ÷↓ g in
                                                         eval t' = eager-map(λx.(x ÷ g);t) in
                                                           inl [[h' / t'] / Ls]
                                                    else (inl [L / Ls]);s';v)))
    ⇒ (cc ∈ sat)
    ⇒ (cc ∈ outl(let s' ⟵ let h,t = u 
                            in if t = Ax then if (h) < (0)  then inr ⋅   else (inl [u / sat])
                               otherwise eval g = |gcd-list(t)| in
                                         if (1) < (g)
                                            then eval h' = h ÷↓ g in
                                                 eval t' = eager-map(λx.(x ÷ g);t) in
                                                   inl [[h' / t'] / sat]
                                            else (inl [u / sat])
                  in accumulate_abort(L,Ls.let h,t = L 
                                           in if t = Ax then if (h) < (0)  then inr ⋅   else (inl [L / Ls])
                                              otherwise eval g = |gcd-list(t)| in
                                                        if (1) < (g)
                                                           then eval h' = h ÷↓ g in
                                                                eval t' = eager-map(λx.(x ÷ g);t) in
                                                                  inl [[h' / t'] / Ls]
                                                           else (inl [L / Ls]);s';v))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}ineqs,sat:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List.  \mforall{}cc:\{L:\mBbbZ{}  List|  ||L||  =  n\}  .
    ((\muparrow{}isl(gcd-reduce-ineq-constraints(sat;ineqs)))
    {}\mRightarrow{}  (cc  \mmember{}  sat)
    {}\mRightarrow{}  (cc  \mmember{}  outl(gcd-reduce-ineq-constraints(sat;ineqs))))


By

---

Latex:
(InductionOnList
  THEN  Unfold  `gcd-reduce-ineq-constraints`  0
  THEN  (RWW  "accumulate\_abort\_cons\_lemma"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto)))

---

Home Index