---

Step * 1 of Lemma compose-tuple-recodings_wf


1. r1 : L:(Type List) ⟶ (L':Type List
                         × h:tuple-type(L) ⟶ tuple-type(L')
                         × {j:tuple-type(L') ⟶ tuple-type(L)| ∀s:tuple-type(L). ((j (h s)) = s ∈ tuple-type(L))} )
2. r2 : L:(Type List) ⟶ (L':Type List
                         × h:tuple-type(L) ⟶ tuple-type(L')
                         × {j:tuple-type(L') ⟶ tuple-type(L)| ∀s:tuple-type(L). ((j (h s)) = s ∈ tuple-type(L))} )
3. L1 : Type List
4. L' : Type List
5. h : tuple-type(L1) ⟶ tuple-type(L')
6. v2 : {j:tuple-type(L') ⟶ tuple-type(L1)| ∀s:tuple-type(L1). ((j (h s)) = s ∈ tuple-type(L1))} 
7. (r1 L1)
= <L', h, v2>
∈ (L':Type List
  × h:tuple-type(L1) ⟶ tuple-type(L')
  × {j:tuple-type(L') ⟶ tuple-type(L1)| ∀s:tuple-type(L1). ((j (h s)) = s ∈ tuple-type(L1))} )
8. L'@0 : Type List
9. h1 : tuple-type(L') ⟶ tuple-type(L'@0)
10. v4 : {j:tuple-type(L'@0) ⟶ tuple-type(L')| ∀s:tuple-type(L'). ((j (h1 s)) = s ∈ tuple-type(L'))} 
11. (r2 L')
= <L'@0, h1, v4>
∈ (L'@0:Type List
  × h:tuple-type(L') ⟶ tuple-type(L'@0)
  × {j:tuple-type(L'@0) ⟶ tuple-type(L')| ∀s:tuple-type(L'). ((j (h s)) = s ∈ tuple-type(L'))} )
12. s : tuple-type(L1)
⊢ ((v2 o v4) (h1 (h s))) = s ∈ tuple-type(L1)
BY
{ (DVar `v2' THEN DVar `v4' THEN Reduce 0 THEN RWO "-3" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  r1  :  L:(Type  List)  {}\mrightarrow{}  (L':Type  List
                                                  \mtimes{}  h:tuple-type(L)  {}\mrightarrow{}  tuple-type(L')
                                                  \mtimes{}  \{j:tuple-type(L')  {}\mrightarrow{}  tuple-type(L)|  \mforall{}s:tuple-type(L).  ((j  (h  s))  =  s)\}  )
2.  r2  :  L:(Type  List)  {}\mrightarrow{}  (L':Type  List
                                                  \mtimes{}  h:tuple-type(L)  {}\mrightarrow{}  tuple-type(L')
                                                  \mtimes{}  \{j:tuple-type(L')  {}\mrightarrow{}  tuple-type(L)|  \mforall{}s:tuple-type(L).  ((j  (h  s))  =  s)\}  )
3.  L1  :  Type  List
4.  L'  :  Type  List
5.  h  :  tuple-type(L1)  {}\mrightarrow{}  tuple-type(L')
6.  v2  :  \{j:tuple-type(L')  {}\mrightarrow{}  tuple-type(L1)|  \mforall{}s:tuple-type(L1).  ((j  (h  s))  =  s)\} 
7.  (r1  L1)  =  <L',  h,  v2>
8.  L'@0  :  Type  List
9.  h1  :  tuple-type(L')  {}\mrightarrow{}  tuple-type(L'@0)
10.  v4  :  \{j:tuple-type(L'@0)  {}\mrightarrow{}  tuple-type(L')|  \mforall{}s:tuple-type(L').  ((j  (h1  s))  =  s)\} 
11.  (r2  L')  =  <L'@0,  h1,  v4>
12.  s  :  tuple-type(L1)
\mvdash{}  ((v2  o  v4)  (h1  (h  s)))  =  s


By

---

Latex:
(DVar  `v2'  THEN  DVar  `v4'  THEN  Reduce  0  THEN  RWO  "-3"  0  THEN  Auto)\mcdot{}

---

Home Index