---

Step * of Lemma qeq-functionality

No Annotations
∀[r,s,x:ℤ ⋃ (ℤ × ℤ-o)].  qeq(r;x) = qeq(s;x) supposing qeq(r;s) = tt
BY
{ (Auto
   THEN All D_rational_form
   THEN All (RepUR ``qeq``)
   THEN RepeatFor 2 ((All CallByValueReduce THENA Auto))
   THEN All Reduce
   THEN All Reduce
   THEN Try (Complete (Auto))) }

1
1. a4 : ℤ
2. a5 : ℤ-o
3. a2 : ℤ
4. a1 : ℤ
5. (a4 =z a2 * a5) = tt
⊢ (a4 =z a1 * a5) = (a2 =z a1)

2
1. a5 : ℤ
2. a3 : ℤ
3. a4 : ℤ-o
4. a1 : ℤ
5. (a5 * a4 =z a3) = tt
⊢ (a5 =z a1) = (a3 =z a1 * a4)

3
1. a6 : ℤ
2. a7 : ℤ-o
3. a3 : ℤ
4. a4 : ℤ-o
5. a1 : ℤ
6. (a6 * a4 =z a3 * a7) = tt
⊢ (a6 =z a1 * a7) = (a3 =z a1 * a4)

4
1. a6 : ℤ
2. a7 : ℤ-o
3. a4 : ℤ
4. a2 : ℤ
5. a3 : ℤ-o
6. (a6 =z a4 * a7) = tt
⊢ (a6 * a3 =z a2 * a7) = (a4 * a3 =z a2)

5
1. a7 : ℤ
2. a5 : ℤ
3. a6 : ℤ-o
4. a2 : ℤ
5. a3 : ℤ-o
6. (a7 * a6 =z a5) = tt
⊢ (a7 * a3 =z a2) = (a5 * a3 =z a2 * a6)

6
1. a8 : ℤ
2. a9 : ℤ-o
3. a5 : ℤ
4. a6 : ℤ-o
5. a2 : ℤ
6. a3 : ℤ-o
7. (a8 * a6 =z a5 * a9) = tt
⊢ (a8 * a3 =z a2 * a9) = (a5 * a3 =z a2 * a6)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r,s,x:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})].    qeq(r;x)  =  qeq(s;x)  supposing  qeq(r;s)  =  tt


By

---

Latex:
(Auto
  THEN  All  D\_rational\_form
  THEN  All  (RepUR  ``qeq``)
  THEN  RepeatFor  2  ((All  CallByValueReduce  THENA  Auto))
  THEN  All  Reduce
  THEN  All  Reduce
  THEN  Try  (Complete  (Auto)))

---

Home Index