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