---

Step * 1 1 1 of Lemma append_functionality_wrt_permutation

.....subterm..... T:t
1:n
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 : ℕ||as1|| + ||as2||@i
⊢ if i <z ||as1|| then f1 i else ||as1|| + (f (i - ||as1||)) fi  ∈ ℕ||as1|| + ||as2||
BY
{ TACTIC:(SplitOnConclITE THENA Auto) }

1
.....truecase..... 
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 : ℕ||as1|| + ||as2||@i
15. i < ||as1||
⊢ f1 i ∈ ℕ||as1|| + ||as2||

2
.....falsecase..... 
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 : ℕ||as1|| + ||as2||@i
15. ||as1|| ≤ i
⊢ ||as1|| + (f (i - ||as1||)) ∈ ℕ||as1|| + ||as2||

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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.  i  :  \mBbbN{}||as1||  +  ||as2||@i
\mvdash{}  if  i  <z  ||as1||  then  f1  i  else  ||as1||  +  (f  (i  -  ||as1||))  fi    \mmember{}  \mBbbN{}||as1||  +  ||as2||


By

---

Latex:
TACTIC:(SplitOnConclITE  THENA  Auto)

---

Home Index