---

Step * 1 1 of Lemma qinv_wf

.....antecedent..... 
1. istype(ℤ ⋃ (ℤ × ℤ-o))
2. ∀r1,s:ℤ ⋃ (ℤ × ℤ-o).  istype(qeq(r1;s) = tt)
3. ∀r1:ℤ ⋃ (ℤ × ℤ-o). qeq(r1;r1) = tt
4. a : Base
5. b : Base
6. c : a = b ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
7. a ∈ ℤ ⋃ (ℤ × ℤ-o)
8. b ∈ ℤ ⋃ (ℤ × ℤ-o)
9. qeq(a;b) = tt
10. ¬↑qeq(a;0)
11. qeq(a;0) = qeq(b;0)
⊢ qeq(1/a;1/b) = tt
BY
{ (Thin (-1)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclTerm ⌜a⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜b⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN All D_rational_form) }

1
1. a2 : ℤ
2. a1 : ℤ
3. qeq(a2;a1) = tt
4. ¬↑qeq(a2;0)
⊢ qeq(1/a2;1/a1) = tt

2
1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
4. qeq(<a3, a4>;a1) = tt
5. ¬↑qeq(<a3, a4>;0)
⊢ qeq(1/<a3, a4>;1/a1) = tt

3
1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
4. qeq(a4;<a2, a3>) = tt
5. ¬↑qeq(a4;0)
⊢ qeq(1/a4;1/<a2, a3>) = tt

4
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
5. qeq(<a5, a6>;<a2, a3>) = tt
6. ¬↑qeq(<a5, a6>;0)
⊢ qeq(1/<a5, a6>;1/<a2, a3>) = tt

---

Latex:

---

Latex:
.....antecedent..... 
1.  istype(\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}))
2.  \mforall{}r1,s:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}).    istype(qeq(r1;s)  =  tt)
3.  \mforall{}r1:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}).  qeq(r1;r1)  =  tt
4.  a  :  Base
5.  b  :  Base
6.  c  :  a  =  b
7.  a  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
8.  b  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
9.  qeq(a;b)  =  tt
10.  \mneg{}\muparrow{}qeq(a;0)
11.  qeq(a;0)  =  qeq(b;0)
\mvdash{}  qeq(1/a;1/b)  =  tt


By

---

Latex:
(Thin  (-1)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  All  D\_rational\_form)

---

Home Index