---

Step * 1 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|| ∈ ℤ
⊢ ∃f:ℕ||as1 @ as2|| ⟶ ℕ||as1 @ as2||
   (Inj(ℕ||as1 @ as2||;ℕ||as1 @ as2||;f) ∧ ((bs1 @ bs2) = (as1 @ as2 o f) ∈ (A List)))
BY
{ TACTIC:((RWO "length-append" 0 THENA Auto)
          THEN Assert ⌜λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi  ∈ ℕ||as1|| + ||as2||
                       ⟶ ℕ||as1|| + ||as2||⌝⋅
          ) }

1
.....assertion..... 
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|| ∈ ℤ
⊢ λi.if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi  ∈ ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||

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||
⊢ ∃f:ℕ||as1|| + ||as2|| ⟶ ℕ||as1|| + ||as2||
   (Inj(ℕ||as1|| + ||as2||;ℕ||as1|| + ||as2||;f) ∧ ((bs1 @ bs2) = (as1 @ as2 o f) ∈ (A List)))

---

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||
\mvdash{}  \mexists{}f:\mBbbN{}||as1  @  as2||  {}\mrightarrow{}  \mBbbN{}||as1  @  as2||
      (Inj(\mBbbN{}||as1  @  as2||;\mBbbN{}||as1  @  as2||;f)  \mwedge{}  ((bs1  @  bs2)  =  (as1  @  as2  o  f)))


By

---

Latex:
TACTIC:((RWO  "length-append"  0  THENA  Auto)
                THEN  Assert  \mkleeneopen{}\mlambda{}i.if  i  <z  ||as1||  then  f1  i  else  ||as1||  +  (f  (i  -  ||as1||))  fi    \mmember{}  \mBbbN{}||as1||
                                          +  ||as2||  {}\mrightarrow{}  \mBbbN{}||as1||  +  ||as2||\mkleeneclose{}\mcdot{}
                )

---

Home Index