Step * 1 of Lemma lg-append_wf


1. Type
2. g1 self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g2 self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
⊢ 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) ∈ self:Top \000CList ∩ (T
                                                                                        × ℕ||self|| List
                                                                                        × (ℕ||self|| List)) List
BY
(DepIsectHD (-2)
   THEN DepIsectHD (-1)
   THEN (Assert ||g1|| ∈ ℤ BY
               (GenConcl ⌈g1 G1 ∈ (Top List)⌉⋅⋅ THEN Auto))
   THEN (Assert ||g2|| ∈ ℤ BY
               (GenConcl ⌈g2 G2 ∈ (Top List)⌉⋅⋅ THEN Auto))) }

1
1. 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) ∈ self:Top \000CList ∩ (T
                                                                                        × ℕ||self|| List
                                                                                        × (ℕ||self|| List)) List


Latex:



Latex:

1.  T  :  Type
2.  g1  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
3.  g2  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
\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{}  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List


By


Latex:
(DepIsectHD  (-2)
  THEN  DepIsectHD  (-1)
  THEN  (Assert  ||g1||  \mmember{}  \mBbbZ{}  BY
                          (GenConcl  \mkleeneopen{}g1  =  G1\mkleeneclose{}\mcdot{}\mcdot{}  THEN  Auto))
  THEN  (Assert  ||g2||  \mmember{}  \mBbbZ{}  BY
                          (GenConcl  \mkleeneopen{}g2  =  G2\mkleeneclose{}\mcdot{}\mcdot{}  THEN  Auto)))




Home Index