---

Step * of Lemma decidable__q-constraints2

∀k:ℕ. ∀A:(ℚ List × ℤ × (ℚ List)) List.  Dec(∃y:ℚ List [q-sat-constraints(k;A;y)])
BY
{ xxx(Unfold `q-sat-constraints` 0
      THEN (xxxUnivCDxxx THENA Auto)
      THEN (InstLemma `decidable__q-constraints-opt` [⌜k⌝]⋅
            THENA (Auto THEN D -1 THEN D -1 THEN Reduce 0 THEN Auto)
            ))xxx }

1
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])
⊢ Dec(∃y:ℚ List [((||y|| = k ∈ ℤ)
                c∧ (∀a∈A.let F,r,G = a in 
                      if (r =z 0) then q-linear(k;j.F[j]?0;y) = q-linear(k;j.G[j]?0;y) ∈ ℚ
                      if (r =z 1) then q-linear(k;j.F[j]?0;y) ≤ q-linear(k;j.G[j]?0;y)
                      else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
                      fi ))])

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}A:(\mBbbQ{}  List  \mtimes{}  \mBbbZ{}  \mtimes{}  (\mBbbQ{}  List))  List.    Dec(\mexists{}y:\mBbbQ{}  List  [q-sat-constraints(k;A;y)])


By

---

Latex:
xxx(Unfold  `q-sat-constraints`  0
        THEN  (xxxUnivCDxxx  THENA  Auto)
        THEN  (InstLemma  `decidable\_\_q-constraints-opt`  [\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
                    THENA  (Auto  THEN  D  -1  THEN  D  -1  THEN  Reduce  0  THEN  Auto)
                    ))xxx

---

Home Index