---

Step * 1 of Lemma norm-list_wf_sq


1. T : Type
2. T ⊆r Base
3. value-type(T)
4. N : sq-id-fun(T)
5. SQType(T List)
6. SQType(T)
7. L : T List
⊢ norm-list(N) L ∈ {y:T List| L ~ y} 
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 (Assert value-type(T List) BY
               Auto)
   THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))) }

1
1. T : Type
2. T ⊆r Base
3. value-type(T)
4. N : sq-id-fun(T)
5. SQType(T List)
6. SQType(T)
7. u : T
8. v : T List
9. norm-list(N) v ∈ {y:T List| v ~ y} 
10. value-type(T List)
⊢ [u / v] = [N u / (norm-list(N) v)] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  value-type(T)
4.  N  :  sq-id-fun(T)
5.  SQType(T  List)
6.  SQType(T)
7.  L  :  T  List
\mvdash{}  norm-list(N)  L  \mmember{}  \{y:T  List|  L  \msim{}  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  (Assert  value-type(T  List)  BY
                          Auto)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto)))

---

Home Index