---

Step * 1 1 2 2 of Lemma lg-append_wf


1. T : Type
2. g1 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g1 ∈ Top List
4. g1 ∈ (T × ℕ||g1|| List × (ℕ||g1|| List)) List
5. g2 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
6. g2 ∈ Top List
7. g2 ∈ (T × ℕ||g2|| List × (ℕ||g2|| List)) List
8. ||g1|| ∈ ℤ
9. ||g2|| ∈ ℤ
⊢ g1 @ map(λtr.let lbl,in,out = tr in <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2) ∈ (T
  × ℕ||g1|| + ||g2|| List
  × (ℕ||g1|| + ||g2|| List)) List
BY
{ MemCD }

1
.....implicit subterm..... 
1. T : Type
2. g1 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g1 ∈ Top List
4. g1 ∈ (T × ℕ||g1|| List × (ℕ||g1|| List)) List
5. g2 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
6. g2 ∈ Top List
7. g2 ∈ (T × ℕ||g2|| List × (ℕ||g2|| List)) List
8. ||g1|| ∈ ℤ
9. ||g2|| ∈ ℤ
⊢ T × ℕ||g1|| + ||g2|| List × (ℕ||g1|| + ||g2|| List) ∈ Type

2
.....subterm..... T:t
1:n
1. T : Type
2. g1 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g1 ∈ Top List
4. g1 ∈ (T × ℕ||g1|| List × (ℕ||g1|| List)) List
5. g2 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
6. g2 ∈ Top List
7. g2 ∈ (T × ℕ||g2|| List × (ℕ||g2|| List)) List
8. ||g1|| ∈ ℤ
9. ||g2|| ∈ ℤ
⊢ g1 ∈ (T × ℕ||g1|| + ||g2|| List × (ℕ||g1|| + ||g2|| List)) List

3
.....subterm..... T:t
2:n
1. T : Type
2. g1 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g1 ∈ Top List
4. g1 ∈ (T × ℕ||g1|| List × (ℕ||g1|| List)) List
5. g2 : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
6. g2 ∈ Top List
7. g2 ∈ (T × ℕ||g2|| List × (ℕ||g2|| List)) List
8. ||g1|| ∈ ℤ
9. ||g2|| ∈ ℤ
⊢ map(λtr.let lbl,in,out = tr in 
          <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>;g2) ∈ (T
  × ℕ||g1|| + ||g2|| List
  × (ℕ||g1|| + ||g2|| List)) List

---

Latex:

---

Latex:

1.  T  :  Type
2.  g1  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
3.  g1  \mmember{}  Top  List
4.  g1  \mmember{}  (T  \mtimes{}  \mBbbN{}||g1||  List  \mtimes{}  (\mBbbN{}||g1||  List))  List
5.  g2  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
6.  g2  \mmember{}  Top  List
7.  g2  \mmember{}  (T  \mtimes{}  \mBbbN{}||g2||  List  \mtimes{}  (\mBbbN{}||g2||  List))  List
8.  ||g1||  \mmember{}  \mBbbZ{}
9.  ||g2||  \mmember{}  \mBbbZ{}
\mvdash{}  g1
    @  map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                        <lbl,  map(\mlambda{}x.(x  +  lg-size(g1));in),  map(\mlambda{}x.(x  +  lg-size(g1));out)>g2)  \mmember{}  (T
    \mtimes{}  \mBbbN{}||g1||  +  ||g2||  List
    \mtimes{}  (\mBbbN{}||g1||  +  ||g2||  List))  List


By

---

Latex:
MemCD

---

Home Index