---

Step * 1 1 of Lemma cons_cancel_wrt_permutation

.....assertion..... 
1. [A] : Type
2. a : A
3. bs : A List
4. cs : A List
5. f : ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
6. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;f)
7. [a / cs] = ([a / bs] o f) ∈ (A List)
8. ||[a / bs]|| = ||[a / cs]|| ∈ ℤ
9. ||bs|| = ||cs|| ∈ ℤ
⊢ ∃g:ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
   (Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;g) ∧ ([a / cs] = ([a / bs] o g) ∈ (A List)) ∧ ((g 0) = 0 ∈ ℤ))
BY
{ ((Assert 0 < ||[a / bs]|| BY Auto') THEN InstConcl [⌜(0, f 0) o f⌝]⋅ THEN Auto') }

1
1. [A] : Type
2. a : A
3. bs : A List
4. cs : A List
5. f : ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
6. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;f)
7. [a / cs] = ([a / bs] o f) ∈ (A List)
8. ||[a / bs]|| = ||[a / cs]|| ∈ ℤ
9. ||bs|| = ||cs|| ∈ ℤ
10. 0 < ||[a / bs]||
⊢ Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;(0, f 0) o f)

2
1. A : Type
2. a : A
3. bs : A List
4. cs : A List
5. f : ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
6. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;f)
7. [a / cs] = ([a / bs] o f) ∈ (A List)
8. ||[a / bs]|| = ||[a / cs]|| ∈ ℤ
9. ||bs|| = ||cs|| ∈ ℤ
10. 0 < ||[a / bs]||
11. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;(0, f 0) o f)
⊢ [a / cs] = ([a / bs] o (0, f 0) o f) ∈ (A List)

3
1. A : Type
2. a : A
3. bs : A List
4. cs : A List
5. f : ℕ||[a / bs]|| ⟶ ℕ||[a / bs]||
6. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;f)
7. [a / cs] = ([a / bs] o f) ∈ (A List)
8. ||[a / bs]|| = ||[a / cs]|| ∈ ℤ
9. ||bs|| = ||cs|| ∈ ℤ
10. 0 < ||[a / bs]||
11. Inj(ℕ||[a / bs]||;ℕ||[a / bs]||;(0, f 0) o f)
12. [a / cs] = ([a / bs] o (0, f 0) o f) ∈ (A List)
⊢ (((0, f 0) o f) 0) = 0 ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Type
2.  a  :  A
3.  bs  :  A  List
4.  cs  :  A  List
5.  f  :  \mBbbN{}||[a  /  bs]||  {}\mrightarrow{}  \mBbbN{}||[a  /  bs]||
6.  Inj(\mBbbN{}||[a  /  bs]||;\mBbbN{}||[a  /  bs]||;f)
7.  [a  /  cs]  =  ([a  /  bs]  o  f)
8.  ||[a  /  bs]||  =  ||[a  /  cs]||
9.  ||bs||  =  ||cs||
\mvdash{}  \mexists{}g:\mBbbN{}||[a  /  bs]||  {}\mrightarrow{}  \mBbbN{}||[a  /  bs]||
      (Inj(\mBbbN{}||[a  /  bs]||;\mBbbN{}||[a  /  bs]||;g)  \mwedge{}  ([a  /  cs]  =  ([a  /  bs]  o  g))  \mwedge{}  ((g  0)  =  0))


By

---

Latex:
((Assert  0  <  ||[a  /  bs]||  BY  Auto')  THEN  InstConcl  [\mkleeneopen{}(0,  f  0)  o  f\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index