---

Step * of Lemma sublist_append

No Annotations
∀[T:Type]. ∀L1,L2,L1',L2':T List.  (L1 ⊆ L1' ⇒ L2 ⊆ L2' ⇒ L1 @ L2 ⊆ L1' @ L2')
BY
{ (((Auto THEN All (Unfold `sublist`)) THEN ExRepD)
   THEN InstConcl [λi.if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi ]
   ) }

1
.....wf..... 
1. T : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L1'||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L1'[f1 j] ∈ T)
9. f : ℕ||L2|| ⟶ ℕ||L2'||
10. increasing(f;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
⊢ λi.if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi  ∈ ℕ||L1 @ L2|| ⟶ ℕ||L1' @ L2'||

2
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L1'||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L1'[f1 j] ∈ T)
9. f : ℕ||L2|| ⟶ ℕ||L2'||
10. increasing(f;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
⊢ increasing(λi.if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi ;||L1 @ L2||)
∧ (∀j:ℕ||L1 @ L2||. (L1 @ L2[j] = L1' @ L2'[(λi.if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi ) j] ∈ T))

3
.....wf..... 
1. T : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L1'||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L1'[f1 j] ∈ T)
9. f : ℕ||L2|| ⟶ ℕ||L2'||
10. increasing(f;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
12. f2 : ℕ||L1 @ L2|| ⟶ ℕ||L1' @ L2'||
⊢ istype(increasing(f2;||L1 @ L2||) ∧ (∀j:ℕ||L1 @ L2||. (L1 @ L2[j] = L1' @ L2'[f2 j] ∈ T)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}L1,L2,L1',L2':T  List.    (L1  \msubseteq{}  L1'  {}\mRightarrow{}  L2  \msubseteq{}  L2'  {}\mRightarrow{}  L1  @  L2  \msubseteq{}  L1'  @  L2')


By

---

Latex:
(((Auto  THEN  All  (Unfold  `sublist`))  THEN  ExRepD)
  THEN  InstConcl  [\mlambda{}i.if  i  <z  ||L1||  then  f1  i  else  (f  (i  -  ||L1||))  +  ||L1'||  fi  ]
  )

---

Home Index