---

Step * 1 1 1 1 1 1 of Lemma disjoint_increasing_onto


1. m : ℕ
2. n : ℕ
3. k : ℕ
4. f : ℕn ⟶ ℕm
5. g : ℕk ⟶ ℕm
6. increasing(f;n)
7. increasing(g;k)
8. h : i:ℕm ⟶ (j:ℕn × (i = (f j) ∈ ℤ) + (j:ℕk × (i = (g j) ∈ ℤ)))
9. ∀j1:ℕn. ∀j2:ℕk.  (¬((f j1) = (g j2) ∈ ℤ))
10. a1 : ℕm
11. a2 : ℕm
⊢ (case h a1 of inl(p) => fst(p) | inr(p) => n + (fst(p))
= case h a2 of inl(p) => fst(p) | inr(p) => n + (fst(p))
∈ ℕn + k)
⇒ (a1 = a2 ∈ ℕm)
BY
{ (((GenConcl (h a1) = q1 ∈ (j:ℕn × (a1 = (f j) ∈ ℤ) + (j:ℕk × (a1 = (g j) ∈ ℤ))) THENA Auto{1,3}-1)
    THEN GenConcl (h a2) = q2 ∈ (j:ℕn × (a2 = (f j) ∈ ℤ) + (j:ℕk × (a2 = (g j) ∈ ℤ)))
    )
   THENA Auto
   ) }

1
1. m : ℕ
2. n : ℕ
3. k : ℕ
4. f : ℕn ⟶ ℕm
5. g : ℕk ⟶ ℕm
6. increasing(f;n)
7. increasing(g;k)
8. h : i:ℕm ⟶ (j:ℕn × (i = (f j) ∈ ℤ) + (j:ℕk × (i = (g j) ∈ ℤ)))
9. ∀j1:ℕn. ∀j2:ℕk.  (¬((f j1) = (g j2) ∈ ℤ))
10. a1 : ℕm
11. a2 : ℕm
12. q1 : j:ℕn × (a1 = (f j) ∈ ℤ) + (j:ℕk × (a1 = (g j) ∈ ℤ))
13. (h a1) = q1 ∈ (j:ℕn × (a1 = (f j) ∈ ℤ) + (j:ℕk × (a1 = (g j) ∈ ℤ)))
14. q2 : j:ℕn × (a2 = (f j) ∈ ℤ) + (j:ℕk × (a2 = (g j) ∈ ℤ))
15. (h a2) = q2 ∈ (j:ℕn × (a2 = (f j) ∈ ℤ) + (j:ℕk × (a2 = (g j) ∈ ℤ)))
⊢ (case q1 of inl(p) => fst(p) | inr(p) => n + (fst(p)) = case q2 of inl(p) => fst(p) | inr(p) => n + (fst(p)) ∈ ℕn + k)
⇒ (a1 = a2 ∈ ℕm)

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  k  :  \mBbbN{}
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m
5.  g  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m
6.  increasing(f;n)
7.  increasing(g;k)
8.  h  :  i:\mBbbN{}m  {}\mrightarrow{}  (j:\mBbbN{}n  \mtimes{}  (i  =  (f  j))  +  (j:\mBbbN{}k  \mtimes{}  (i  =  (g  j))))
9.  \mforall{}j1:\mBbbN{}n.  \mforall{}j2:\mBbbN{}k.    (\mneg{}((f  j1)  =  (g  j2)))
10.  a1  :  \mBbbN{}m
11.  a2  :  \mBbbN{}m
\mvdash{}  (case  h  a1  of  inl(p)  =>  fst(p)  |  inr(p)  =>  n  +  (fst(p))
=  case  h  a2  of  inl(p)  =>  fst(p)  |  inr(p)  =>  n  +  (fst(p)))
{}\mRightarrow{}  (a1  =  a2)


By

---

Latex:
(((GenConcl  (h  a1)  =  q1  THENA  Auto\{1,3\}-1)  THEN  GenConcl  (h  a2)  =  q2)  THENA  Auto)

---

Home Index