---

Step * of Lemma compose-tuple-recodings_wf

∀[r1,r2:TupleRecoding].  (r2 o r1 ∈ TupleRecoding)
BY
{ xxx(RepUR ``tuple-recoding compose-tuple-recodings`` 0
      THEN Auto
      THEN RepeatFor 2 ((GenConclAtAddr [2;1] THEN Auto))
      THEN MemTypeCD
      THEN Auto)xxx }

1
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)

---

Latex:

---

Latex:
\mforall{}[r1,r2:TupleRecoding].    (r2  o  r1  \mmember{}  TupleRecoding)


By

---

Latex:
xxx(RepUR  ``tuple-recoding  compose-tuple-recodings``  0
        THEN  Auto
        THEN  RepeatFor  2  ((GenConclAtAddr  [2;1]  THEN  Auto))
        THEN  MemTypeCD
        THEN  Auto)xxx

---

Home Index