---

Step * of Lemma chinese-remainder2

∀r,s,a,b:ℤ.  Dec(∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))])
BY
{ xxx(Auto
      THEN (InstLemma `gcd-reduce` [⌜r⌝;⌜s⌝]⋅ THENA Auto)
      THEN ExRepD
      THEN UseWitness ⌜if (g =z 0) then if (a =z b) then inl a else inr (λx.⋅)  fi 
                       if (b - a rem g =z 0) then eval z = a + (x * ((b - a) ÷ g) * r) in inl z
                       else inr (λx.⋅) 
                       fi ⌝⋅
      THEN Repeat ((SplitOnConclITE THENA Auto))
      THEN RepUR ``decidable or not sq_exists`` 0⋅
      THEN Try (((MemCD THENA Auto) THEN Unfold `implies` 0 THEN MemCD THEN Auto THEN D -1))
      THEN Try ((Auto THEN MemTypeCD THEN Auto THEN RelRST THEN Auto)))xxx }

1
1. r : ℤ
2. s : ℤ
3. a : ℤ
4. b : ℤ
5. g : ℕ
6. a1 : ℤ
7. b1 : ℤ
8. x : ℤ
9. y : ℤ
10. r = (a1 * g) ∈ ℤ
11. s = (b1 * g) ∈ ℤ
12. ((x * a1) + (y * b1)) = 1 ∈ ℤ
13. g = 0 ∈ ℤ
14. ¬(a = b ∈ ℤ)
15. x1 : ℤ
16. (x1 ≡ a mod r) ∧ (x1 ≡ b mod s)
⊢ ⋅ ∈ False

2
1. r : ℤ
2. s : ℤ
3. a : ℤ
4. b : ℤ
5. g : ℕ
6. a1 : ℤ
7. b1 : ℤ
8. x : ℤ
9. y : ℤ
10. r = (a1 * g) ∈ ℤ
11. s = (b1 * g) ∈ ℤ
12. ((x * a1) + (y * b1)) = 1 ∈ ℤ
13. ¬(g = 0 ∈ ℤ)
14. (b - a rem g) = 0 ∈ ℤ
⊢ eval z = a + (x * ((b - a) ÷ g) * r) in
  inl z ∈ {x:ℤ| (x ≡ a mod r) ∧ (x ≡ b mod s)}  + ({x:ℤ| (x ≡ a mod r) ∧ (x ≡ b mod s)}  ⇒ False)

3
1. r : ℤ
2. s : ℤ
3. a : ℤ
4. b : ℤ
5. g : ℕ
6. a1 : ℤ
7. b1 : ℤ
8. x : ℤ
9. y : ℤ
10. r = (a1 * g) ∈ ℤ
11. s = (b1 * g) ∈ ℤ
12. ((x * a1) + (y * b1)) = 1 ∈ ℤ
13. ¬(g = 0 ∈ ℤ)
14. ¬((b - a rem g) = 0 ∈ ℤ)
15. x1 : ℤ
16. (x1 ≡ a mod r) ∧ (x1 ≡ b mod s)
⊢ ⋅ ∈ False

---

Latex:

---

Latex:
\mforall{}r,s,a,b:\mBbbZ{}.    Dec(\mexists{}x:\mBbbZ{}  [((x  \mequiv{}  a  mod  r)  \mwedge{}  (x  \mequiv{}  b  mod  s))])


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `gcd-reduce`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  ExRepD
        THEN  UseWitness  \mkleeneopen{}if  (g  =\msubz{}  0)  then  if  (a  =\msubz{}  b)  then  inl  a  else  inr  (\mlambda{}x.\mcdot{})    fi 
                                          if  (b  -  a  rem  g  =\msubz{}  0)  then  eval  z  =  a  +  (x  *  ((b  -  a)  \mdiv{}  g)  *  r)  in  inl  z
                                          else  inr  (\mlambda{}x.\mcdot{}) 
                                          fi  \mkleeneclose{}\mcdot{}
        THEN  Repeat  ((SplitOnConclITE  THENA  Auto))
        THEN  RepUR  ``decidable  or  not  sq\_exists``  0\mcdot{}
        THEN  Try  (((MemCD  THENA  Auto)  THEN  Unfold  `implies`  0  THEN  MemCD  THEN  Auto  THEN  D  -1))
        THEN  Try  ((Auto  THEN  MemTypeCD  THEN  Auto  THEN  RelRST  THEN  Auto)))xxx

---

Home Index