---

Step * 1 2 1 2 of Lemma lg-remove-noop


1. T : Type
2. x : ℕ
3. v : ℕ@i
4. L : (T × ℕv List × (ℕv List)) List@i
5. v ≤ x@i
6. ||L|| ≤ x@i
⊢ map(λtr.let lbl,in,out = tr in 
          <lbl
          , map(λx@0.if x@0 ≤z x then x@0 else x@0 - 1 fi ;filter(λx@0.(¬b(x@0 =z x));in))
          , map(λx@0.if x@0 ≤z x then x@0 else x@0 - 1 fi ;filter(λx@0.(¬b(x@0 =z x));out))>;L) ~ L
BY
{ (Thin (-1)
   THEN ListInd (-2)
   THEN Reduce 0
   THEN EqCD
   THEN Try (Trivial)
   THEN DVar `u'
   THEN DVar `u2'
   THEN Reduce 0
   THEN RepeatFor 2 (EqCD)
   THEN Lemmaize [4]
   THEN (UnivCD THENA Auto)
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN RepeatFor 2 (AutoSplit)
   THEN EqCD
   THEN Try (Trivial)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  \mBbbN{}
3.  v  :  \mBbbN{}@i
4.  L  :  (T  \mtimes{}  \mBbbN{}v  List  \mtimes{}  (\mBbbN{}v  List))  List@i
5.  v  \mleq{}  x@i
6.  ||L||  \mleq{}  x@i
\mvdash{}  map(\mlambda{}tr.let  lbl,in,out  =  tr  in 
                    <lbl
                    ,  map(\mlambda{}x@0.if  x@0  \mleq{}z  x  then  x@0  else  x@0  -  1  fi  ;filter(\mlambda{}x@0.(\mneg{}\msubb{}(x@0  =\msubz{}  x));in))
                    ,  map(\mlambda{}x@0.if  x@0  \mleq{}z  x  then  x@0  else  x@0  -  1  fi  ;filter(\mlambda{}x@0.(\mneg{}\msubb{}(x@0  =\msubz{}  x));out))>L)  \msim{}  L


By

---

Latex:
(Thin  (-1)
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  DVar  `u'
  THEN  DVar  `u2'
  THEN  Reduce  0
  THEN  RepeatFor  2  (EqCD)
  THEN  Lemmaize  [4]
  THEN  (UnivCD  THENA  Auto)
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index