---

Step * 1 2 2 of Lemma append_functionality_wrt_permutation


1. A : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi  ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
⊢ (bs1 @ bs2) = (as1 @ as2 o λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi ) ∈ (A List)
BY
{ TACTIC:(BLemma `list_extensionality` THEN Auto)⋅ }

1
1. A : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi  ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
⊢ (||bs1|| + ||bs2||) = ||(as1 @ as2 o λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi )|| ∈ ℤ

2
1. A : Type
2. as1 : A List@i
3. as2 : A List@i
4. bs1 : A List@i
5. bs2 : A List@i
6. f1 : ℕ||as1|| ⟶ ℕ||as1||@i
7. Inj(ℕ||as1||;ℕ||as1||;f1)
8. bs1 = (as1 o f1) ∈ (A List)
9. f : ℕ||as2|| ⟶ ℕ||as2||@i
10. Inj(ℕ||as2||;ℕ||as2||;f)
11. bs2 = (as2 o f) ∈ (A List)
12. ||as1|| = ||bs1|| ∈ ℤ
13. ||as2|| = ||bs2|| ∈ ℤ
14. λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi  ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
15. i : ℕ@i
16. i < ||bs1 @ bs2||
⊢ bs1 @ bs2[i] = (as1 @ as2 o λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi )[i] ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  as1  :  A  List@i
3.  as2  :  A  List@i
4.  bs1  :  A  List@i
5.  bs2  :  A  List@i
6.  f1  :  \mBbbN{}||as1||  {}\mrightarrow{}  \mBbbN{}||as1||@i
7.  Inj(\mBbbN{}||as1||;\mBbbN{}||as1||;f1)
8.  bs1  =  (as1  o  f1)
9.  f  :  \mBbbN{}||as2||  {}\mrightarrow{}  \mBbbN{}||as2||@i
10.  Inj(\mBbbN{}||as2||;\mBbbN{}||as2||;f)
11.  bs2  =  (as2  o  f)
12.  ||as1||  =  ||bs1||
13.  ||as2||  =  ||bs2||
14.  \mlambda{}i.if  i  <z  ||as1||  then  f1  i  else  ||as1||  +  (f  (i  -  ||as1||))  fi    \mmember{}  \mBbbN{}||as1||  +  ||as2||
        {}\mrightarrow{}  \mBbbN{}||as1||  +  ||as2||
\mvdash{}  (bs1  @  bs2)  =  (as1  @  as2  o  \mlambda{}i.if  i  <z  ||as1||  then  f1  i  else  ||as1||  +  (f  (i  -  ||as1||))  fi  )


By

---

Latex:
TACTIC:(BLemma  `list\_extensionality`  THEN  Auto)\mcdot{}

---

Home Index