---

Step * 1 2 1 2 1 1 1 1 of Lemma recode-tuple_wf


1. f : T:Type ⟶ (L:Type List × h:T ⟶ tuple-type(L) × {j:tuple-type(L) ⟶ T| ∀s:T. ((j (h s)) = s ∈ T)} )
2. u : Type
3. v : Type List
4. h : tuple-type(v) ⟶ Unit
5. v3 : Unit ⟶ tuple-type(v)
6. ∀s:tuple-type(v). ((v3 (h s)) = s ∈ tuple-type(v))
7. L : Type List
8. h1 : u ⟶ tuple-type(L)
9. v6 : tuple-type(L) ⟶ u
10. ∀s:u. ((v6 (h1 s)) = s ∈ u)
11. null(v) = ff
12. ¬0 < 0
13. s1 : u
14. s2 : tuple-type(v)
15. ||L|| = 0 ∈ ℤ
⊢ (v6 (h s2)) = s1 ∈ u
BY
{ (DVar `L'⋅ THEN All Reduce) }

1
1. f : T:Type ⟶ (L:Type List × h:T ⟶ tuple-type(L) × {j:tuple-type(L) ⟶ T| ∀s:T. ((j (h s)) = s ∈ T)} )
2. u : Type
3. v : Type List
4. h : tuple-type(v) ⟶ Unit
5. v3 : Unit ⟶ tuple-type(v)
6. ∀s:tuple-type(v). ((v3 (h s)) = s ∈ tuple-type(v))
7. h1 : u ⟶ Unit
8. v6 : Unit ⟶ u
9. ∀s:u. ((v6 (h1 s)) = s ∈ u)
10. null(v) = ff
11. ¬0 < 0
12. s1 : u
13. s2 : tuple-type(v)
14. 0 = 0 ∈ ℤ
⊢ (v6 (h s2)) = s1 ∈ u

2
1. f : T:Type ⟶ (L:Type List × h:T ⟶ tuple-type(L) × {j:tuple-type(L) ⟶ T| ∀s:T. ((j (h s)) = s ∈ T)} )
2. u : Type
3. v : Type List
4. h : tuple-type(v) ⟶ Unit
5. v3 : Unit ⟶ tuple-type(v)
6. ∀s:tuple-type(v). ((v3 (h s)) = s ∈ tuple-type(v))
7. u1 : Type
8. v7 : Type List
9. h1 : u ⟶ if null(v7) then u1 else u1 × tuple-type(v7) fi 
10. v6 : if null(v7) then u1 else u1 × tuple-type(v7) fi  ⟶ u
11. ∀s:u. ((v6 (h1 s)) = s ∈ u)
12. null(v) = ff
13. ¬0 < 0
14. s1 : u
15. s2 : tuple-type(v)
16. (||v7|| + 1) = 0 ∈ ℤ
⊢ (v6 (h s2)) = s1 ∈ u

---

Latex:

---

Latex:

1.  f  :  T:Type  {}\mrightarrow{}  (L:Type  List
                                  \mtimes{}  h:T  {}\mrightarrow{}  tuple-type(L)
                                  \mtimes{}  \{j:tuple-type(L)  {}\mrightarrow{}  T|  \mforall{}s:T.  ((j  (h  s))  =  s)\}  )
2.  u  :  Type
3.  v  :  Type  List
4.  h  :  tuple-type(v)  {}\mrightarrow{}  Unit
5.  v3  :  Unit  {}\mrightarrow{}  tuple-type(v)
6.  \mforall{}s:tuple-type(v).  ((v3  (h  s))  =  s)
7.  L  :  Type  List
8.  h1  :  u  {}\mrightarrow{}  tuple-type(L)
9.  v6  :  tuple-type(L)  {}\mrightarrow{}  u
10.  \mforall{}s:u.  ((v6  (h1  s))  =  s)
11.  null(v)  =  ff
12.  \mneg{}0  <  0
13.  s1  :  u
14.  s2  :  tuple-type(v)
15.  ||L||  =  0
\mvdash{}  (v6  (h  s2))  =  s1


By

---

Latex:
(DVar  `L'\mcdot{}  THEN  All  Reduce)

---

Home Index