Step
*
1
2
1
1
2
1
1
1
of Lemma
injection-is-surjection
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. i : ℕn
5. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
6. ¬(n = 0 ∈ ℤ)
7. ∀a:ℕn. (if f a <z i then f a else (f a) - 1 fi ∈ ℕn - 1)
8. a1 : ℕn
9. if f a1 <z i then f a1 else (f a1) - 1 fi ∈ ℕn - 1
10. a2 : ℕn
11. if f a2 <z i then f a2 else (f a2) - 1 fi ∈ ℕn - 1
12. if f a1 <z i then f a1 else (f a1) - 1 fi = if f a2 <z i then f a2 else (f a2) - 1 fi ∈ ℤ
13. 0 ≤ if f a1 <z i then f a1 else (f a1) - 1 fi < n - 1
⊢ a1 = a2 ∈ ℤ
BY
{ ((SplitOnHypITE -2 THENA Auto) THEN (SplitOnHypITE -3 THENA Auto)) }
1
.....truecase.....
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. i : ℕn
5. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
6. ¬(n = 0 ∈ ℤ)
7. ∀a:ℕn. (if f a <z i then f a else (f a) - 1 fi ∈ ℕn - 1)
8. a1 : ℕn
9. if f a1 <z i then f a1 else (f a1) - 1 fi ∈ ℕn - 1
10. a2 : ℕn
11. if f a2 <z i then f a2 else (f a2) - 1 fi ∈ ℕn - 1
12. (f a1) = (f a2) ∈ ℤ
13. 0 ≤ if f a1 <z i then f a1 else (f a1) - 1 fi < n - 1
14. f a1 < i
15. f a2 < i
⊢ a1 = a2 ∈ ℤ
2
.....falsecase.....
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. i : ℕn
5. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
6. ¬(n = 0 ∈ ℤ)
7. ∀a:ℕn. (if f a <z i then f a else (f a) - 1 fi ∈ ℕn - 1)
8. a1 : ℕn
9. if f a1 <z i then f a1 else (f a1) - 1 fi ∈ ℕn - 1
10. a2 : ℕn
11. if f a2 <z i then f a2 else (f a2) - 1 fi ∈ ℕn - 1
12. (f a1) = ((f a2) - 1) ∈ ℤ
13. 0 ≤ if f a1 <z i then f a1 else (f a1) - 1 fi < n - 1
14. f a1 < i
15. ¬f a2 < i
⊢ a1 = a2 ∈ ℤ
3
.....truecase.....
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. i : ℕn
5. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
6. ¬(n = 0 ∈ ℤ)
7. ∀a:ℕn. (if f a <z i then f a else (f a) - 1 fi ∈ ℕn - 1)
8. a1 : ℕn
9. if f a1 <z i then f a1 else (f a1) - 1 fi ∈ ℕn - 1
10. a2 : ℕn
11. if f a2 <z i then f a2 else (f a2) - 1 fi ∈ ℕn - 1
12. ((f a1) - 1) = (f a2) ∈ ℤ
13. 0 ≤ if f a1 <z i then f a1 else (f a1) - 1 fi < n - 1
14. ¬f a1 < i
15. f a2 < i
⊢ a1 = a2 ∈ ℤ
4
.....falsecase.....
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. i : ℕn
5. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
6. ¬(n = 0 ∈ ℤ)
7. ∀a:ℕn. (if f a <z i then f a else (f a) - 1 fi ∈ ℕn - 1)
8. a1 : ℕn
9. if f a1 <z i then f a1 else (f a1) - 1 fi ∈ ℕn - 1
10. a2 : ℕn
11. if f a2 <z i then f a2 else (f a2) - 1 fi ∈ ℕn - 1
12. ((f a1) - 1) = ((f a2) - 1) ∈ ℤ
13. 0 ≤ if f a1 <z i then f a1 else (f a1) - 1 fi < n - 1
14. ¬f a1 < i
15. ¬f a2 < i
⊢ a1 = a2 ∈ ℤ
Latex:
Latex:
1. n : \mBbbN{}
2. f : \mBbbN{}n {}\mrightarrow{} \mBbbN{}n
3. Inj(\mBbbN{}n;\mBbbN{}n;f)
4. i : \mBbbN{}n
5. \mforall{}a:\mBbbN{}n. (\mneg{}((f a) = i))
6. \mneg{}(n = 0)
7. \mforall{}a:\mBbbN{}n. (if f a <z i then f a else (f a) - 1 fi \mmember{} \mBbbN{}n - 1)
8. a1 : \mBbbN{}n
9. if f a1 <z i then f a1 else (f a1) - 1 fi \mmember{} \mBbbN{}n - 1
10. a2 : \mBbbN{}n
11. if f a2 <z i then f a2 else (f a2) - 1 fi \mmember{} \mBbbN{}n - 1
12. if f a1 <z i then f a1 else (f a1) - 1 fi = if f a2 <z i then f a2 else (f a2) - 1 fi
13. 0 \mleq{} if f a1 <z i then f a1 else (f a1) - 1 fi < n - 1
\mvdash{} a1 = a2
By
Latex:
((SplitOnHypITE -2 THENA Auto) THEN (SplitOnHypITE -3 THENA Auto))
Home
Index