---

Step * of Lemma member-gcd-reduce-constraints

No Annotations
∀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))))
BY
{ (InductionOnList
   THEN Unfold `gcd-reduce-eq-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-eq-constraints(sat;v))) ⇒ (cc ∈ sat) ⇒ (cc ∈ outl(gcd-reduce-eq-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 inl [u / sat] else (inr ⋅ )
                        otherwise eval g = |gcd-list(t)| in
                                  if (1) < (g)
                                     then if h rem g=0
                                          then eval L' = eager-map(λx.(x ÷ g);u) in
                                               inl [L' / sat]
                                          else (inr ⋅ )
                                     else (inl [u / sat])
           in accumulate_abort(L,Ls.let h,t = L 
                                    in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
                                       otherwise eval g = |gcd-list(t)| in
                                                 if (1) < (g)
                                                    then if h rem g=0
                                                         then eval L' = eager-map(λx.(x ÷ g);L) in
                                                              inl [L' / Ls]
                                                         else (inr ⋅ )
                                                    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 inl [u / sat] else (inr ⋅ )
                               otherwise eval g = |gcd-list(t)| in
                                         if (1) < (g)
                                            then if h rem g=0
                                                 then eval L' = eager-map(λx.(x ÷ g);u) in
                                                      inl [L' / sat]
                                                 else (inr ⋅ )
                                            else (inl [u / sat])
                  in accumulate_abort(L,Ls.let h,t = L 
                                           in if t = Ax then if h=0 then inl [L / Ls] else (inr ⋅ )
                                              otherwise eval g = |gcd-list(t)| in
                                                        if (1) < (g)
                                                           then if h rem g=0
                                                                then eval L' = eager-map(λx.(x ÷ g);L) in
                                                                     inl [L' / Ls]
                                                                else (inr ⋅ )
                                                           else (inl [L / Ls]);s';v))))

---

Latex:

---

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


By

---

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

---

Home Index