---

Step * 1 of Lemma norm-list_wf


1. T : Type
2. value-type(T)
3. N : id-fun(T)
4. L : T List
⊢ norm-list(N) L ∈ {y:T List| L = y ∈ (T List)} 
BY
{ (ListInd (-1)
   THEN Unfold `norm-list` 0
   THEN Reduce 0
   THEN Try ((Subst ⌜rec-case(v) of
                     [] => []
                     a::as =>
                      r.eval a' = N a in
                        eval r' = r in
                          [a' / r'] ~ norm-list(N) v⌝ 0⋅
              THEN Try ((RepUR ``norm-list`` 0 THEN Trivial))
              ))
   THEN MemTypeCD
   THEN Auto
   THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))) }

1
1. T : Type
2. value-type(T)
3. N : id-fun(T)
4. u : T
5. v : T List
6. norm-list(N) v ∈ {y:T List| v = y ∈ (T List)} 
⊢ [u / v] = [N u / (norm-list(N) v)] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  N  :  id-fun(T)
4.  L  :  T  List
\mvdash{}  norm-list(N)  L  \mmember{}  \{y:T  List|  L  =  y\} 


By

---

Latex:
(ListInd  (-1)
  THEN  Unfold  `norm-list`  0
  THEN  Reduce  0
  THEN  Try  ((Subst  \mkleeneopen{}rec-case(v)  of
                                      []  =>  []
                                      a::as  =>
                                        r.eval  a'  =  N  a  in
                                            eval  r'  =  r  in
                                                [a'  /  r']  \msim{}  norm-list(N)  v\mkleeneclose{}  0\mcdot{}
                        THEN  Try  ((RepUR  ``norm-list``  0  THEN  Trivial))
                        ))
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto)))

---

Home Index