---

Step * 1 1 of Lemma qeq-wf


1. r : Base
2. r1 : Base
3. r = r1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
4. r ∈ ℤ ⋃ (ℤ × ℤ-o)
5. r1 ∈ ℤ ⋃ (ℤ × ℤ-o)
6. qeq(r;r1) = tt
7. s : Base
8. s1 : Base
9. s = s1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
10. s ∈ ℤ ⋃ (ℤ × ℤ-o)
11. s1 ∈ ℤ ⋃ (ℤ × ℤ-o)
12. qeq(s;s1) = tt
13. ↑qeq(r;s)@i
⊢ ↑qeq(r1;s1)
BY
{ ((All (RWO "eqtt_to_assert<"))
   THEN Auto
   THEN (InstLemma `qeq-equiv` [] THEN D -1 THEN ExRepD THEN UseTrans ⌜s⌝⋅ THEN UseTrans ⌜r⌝⋅)) }

---

Latex:

---

Latex:

1.  r  :  Base
2.  r1  :  Base
3.  r  =  r1
4.  r  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
5.  r1  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
6.  qeq(r;r1)  =  tt
7.  s  :  Base
8.  s1  :  Base
9.  s  =  s1
10.  s  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
11.  s1  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
12.  qeq(s;s1)  =  tt
13.  \muparrow{}qeq(r;s)@i
\mvdash{}  \muparrow{}qeq(r1;s1)


By

---

Latex:
((All  (RWO  "eqtt\_to\_assert<"))
  THEN  Auto
  THEN  (InstLemma  `qeq-equiv`  []  THEN  D  -1  THEN  ExRepD  THEN  UseTrans  \mkleeneopen{}s\mkleeneclose{}\mcdot{}  THEN  UseTrans  \mkleeneopen{}r\mkleeneclose{}\mcdot{}))

---

Home Index