---

Step * 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
⊢ qeq(r;s) = qeq(r1;s1)
BY
{ (BLemma `iff_imp_equal_bool` THEN Auto) }

1
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)

2
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(r1;s1)@i
⊢ ↑qeq(r;s)

---

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
\mvdash{}  qeq(r;s)  =  qeq(r1;s1)


By

---

Latex:
(BLemma  `iff\_imp\_equal\_bool`  THEN  Auto)

---

Home Index