---

Step * 1 2 1 of Lemma nsub_finite'


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. b : ℕn
5. ¬(∃a:ℕn. ((f a) = b ∈ ℕn))
6. ¬(b = (n - 1) ∈ ℤ)
⊢ Inj(ℕn;ℕn - 1;λi.if (f i =z n - 1) then b else f i fi )
BY
{ ((((ParallelOp 3 THEN Reduce 0) THEN ParallelOp 3) THEN ParallelOp (-1))
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   ) }

1
.....truecase..... 
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. ∀a1,a2:ℕn.  (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
4. b : ℕn
5. ¬(∃a:ℕn. ((f a) = b ∈ ℕn))
6. ¬(b = (n - 1) ∈ ℤ)
7. a1 : ℕn
8. ∀a2:ℕn. (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
9. a2 : ℕn
10. ((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn)
11. (f a1) = (n - 1) ∈ ℤ
12. (f a2) = (n - 1) ∈ ℤ
⊢ (b = b ∈ ℕn - 1) ⇒ (a1 = a2 ∈ ℕn)

2
.....falsecase..... 
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. ∀a1,a2:ℕn.  (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
4. b : ℕn
5. ¬(∃a:ℕn. ((f a) = b ∈ ℕn))
6. ¬(b = (n - 1) ∈ ℤ)
7. a1 : ℕn
8. ∀a2:ℕn. (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
9. a2 : ℕn
10. ((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn)
11. (f a1) = (n - 1) ∈ ℤ
12. ¬((f a2) = (n - 1) ∈ ℤ)
⊢ (b = (f a2) ∈ ℕn - 1) ⇒ (a1 = a2 ∈ ℕn)

3
.....truecase..... 
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. ∀a1,a2:ℕn.  (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
4. b : ℕn
5. ¬(∃a:ℕn. ((f a) = b ∈ ℕn))
6. ¬(b = (n - 1) ∈ ℤ)
7. a1 : ℕn
8. ∀a2:ℕn. (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
9. a2 : ℕn
10. ((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn)
11. ¬((f a1) = (n - 1) ∈ ℤ)
12. (f a2) = (n - 1) ∈ ℤ
⊢ ((f a1) = b ∈ ℕn - 1) ⇒ (a1 = a2 ∈ ℕn)

4
.....falsecase..... 
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. ∀a1,a2:ℕn.  (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
4. b : ℕn
5. ¬(∃a:ℕn. ((f a) = b ∈ ℕn))
6. ¬(b = (n - 1) ∈ ℤ)
7. a1 : ℕn
8. ∀a2:ℕn. (((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn))
9. a2 : ℕn
10. ((f a1) = (f a2) ∈ ℕn) ⇒ (a1 = a2 ∈ ℕn)
11. ¬((f a1) = (n - 1) ∈ ℤ)
12. ¬((f a2) = (n - 1) ∈ ℤ)
⊢ ((f a1) = (f a2) ∈ ℕn - 1) ⇒ (a1 = a2 ∈ ℕn)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  b  :  \mBbbN{}n
5.  \mneg{}(\mexists{}a:\mBbbN{}n.  ((f  a)  =  b))
6.  \mneg{}(b  =  (n  -  1))
\mvdash{}  Inj(\mBbbN{}n;\mBbbN{}n  -  1;\mlambda{}i.if  (f  i  =\msubz{}  n  -  1)  then  b  else  f  i  fi  )


By

---

Latex:
((((ParallelOp  3  THEN  Reduce  0)  THEN  ParallelOp  3)  THEN  ParallelOp  (-1))
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  )

---

Home Index