---

Step * 2 2 of Lemma lg-remove_wf


1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ lg-remove(g;x) ∈ (T
  × ℕif x <z ||g|| then ||g|| - 1 else ||g|| fi  List
  × (ℕif x <z ||g|| then ||g|| - 1 else ||g|| fi  List)) List
BY
{ ((Unfold `lg-remove` 0
    THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
    THEN RepeatFor 2 (D (-1))⋅
    THEN Reduce 0
    THEN RepeatFor 2 (MemCD)
    THEN (GenConclAtAddrType ⌈{m:ℕ||g||| ↑¬b(m =z x)}  List⌉ [2;2]⋅
          THENA (Try ((BLemma `filter_wf3` THEN Auto)) THEN Auto)
          )
    THEN Thin (-1)
    THEN MoveToConcl (-1)
    THEN (GenConclTerm ⌈||g||⌉⋅ THENA Auto)
    THEN All Thin
    THEN RenameVar `n' (-1))
   THEN Auto
   THEN AutoSplit
   THEN RW assert_pushdownC (-4)
   THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
3.  g  \mmember{}  Top  List
4.  g  \mmember{}  (T  \mtimes{}  \mBbbN{}||g||  List  \mtimes{}  (\mBbbN{}||g||  List))  List
5.  ||g||  \mmember{}  \mBbbN{}
6.  x  :  \mBbbN{}
\mvdash{}  lg-remove(g;x)  \mmember{}  (T
    \mtimes{}  \mBbbN{}if  x  <z  ||g||  then  ||g||  -  1  else  ||g||  fi    List
    \mtimes{}  (\mBbbN{}if  x  <z  ||g||  then  ||g||  -  1  else  ||g||  fi    List))  List


By

---

Latex:
((Unfold  `lg-remove`  0
    THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
    THEN  RepeatFor  2  (D  (-1))\mcdot{}
    THEN  Reduce  0
    THEN  RepeatFor  2  (MemCD)
    THEN  (GenConclAtAddrType  \mkleeneopen{}\{m:\mBbbN{}||g|||  \muparrow{}\mneg{}\msubb{}(m  =\msubz{}  x)\}    List\mkleeneclose{}  [2;2]\mcdot{}
                THENA  (Try  ((BLemma  `filter\_wf3`  THEN  Auto))  THEN  Auto)
                )
    THEN  Thin  (-1)
    THEN  MoveToConcl  (-1)
    THEN  (GenConclTerm  \mkleeneopen{}||g||\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  All  Thin
    THEN  RenameVar  `n'  (-1))
  THEN  Auto
  THEN  AutoSplit
  THEN  RW  assert\_pushdownC  (-4)
  THEN  Auto')

---

Home Index