---

Step * 1 2 of Lemma hdataflow-equal

.....subterm..... T:t
2:n
1. A : Type
2. B : Type
3. P : corec(P.A ─→ (P × bag(B))?)
4. Q : corec(P.A ─→ (P × bag(B))?)
5. ∀[inputs:A List]
     (hdf-halted(P*(inputs)) = hdf-halted(Q*(inputs))
     ∧ (∀[a:A]. (hdf-out(P*(inputs);a) = hdf-out(Q*(inputs);a) ∈ bag(B))))
6. P1 : Type@i'
7. (A ─→ (P1 × bag(B))?) ⊆r P1@i
8. corec(P.A ─→ (P × bag(B))?) ⊆r P1@i
9. ∀x,y:corec(P.A ─→ (P × bag(B))?).
     ((∀[inputs:A List]
         (hdf-halted(x*(inputs)) = hdf-halted(y*(inputs))
         ∧ (∀[a:A]. (hdf-out(x*(inputs);a) = hdf-out(y*(inputs);a) ∈ bag(B)))))
     ⇒ (x = y ∈ P1))@i
10. x1 : A ─→ (corec(P.A ─→ (P × bag(B))?) × bag(B))@i
11. x : A ─→ (corec(P.A ─→ (P × bag(B))?) × bag(B))@i
12. ∀[inputs:A List]
      (hdf-halted(inl x1*(inputs)) = hdf-halted(inl x*(inputs))
      ∧ (∀[a:A]. (hdf-out(inl x1*(inputs);a) = hdf-out(inl x*(inputs);a) ∈ bag(B))))@i
13. ff = ff
14. ∀[a:A]. (hdf-out(inl x1;a) = hdf-out(inl x;a) ∈ bag(B))
15. a : A
⊢ (snd((x1 a))) = (snd((x a))) ∈ bag(B)
BY
{ ((InstHyp [⌈a⌉] (-2)⋅ THENA Auto) THEN RepUR ``hdf-out hdf-ap`` (-1) THEN Auto)⋅ }

---

Latex:


.....subterm.....  T:t
2:n
1.  A  :  Type
2.  B  :  Type
3.  P  :  corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)
4.  Q  :  corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)
5.  \mforall{}[inputs:A  List]
          (hdf-halted(P*(inputs))  =  hdf-halted(Q*(inputs))
          \mwedge{}  (\mforall{}[a:A].  (hdf-out(P*(inputs);a)  =  hdf-out(Q*(inputs);a))))
6.  P1  :  Type@i'
7.  (A  {}\mrightarrow{}  (P1  \mtimes{}  bag(B))?)  \msubseteq{}r  P1@i
8.  corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)  \msubseteq{}r  P1@i
9.  \mforall{}x,y:corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?).
          ((\mforall{}[inputs:A  List]
                  (hdf-halted(x*(inputs))  =  hdf-halted(y*(inputs))
                  \mwedge{}  (\mforall{}[a:A].  (hdf-out(x*(inputs);a)  =  hdf-out(y*(inputs);a)))))
          {}\mRightarrow{}  (x  =  y))@i
10.  x1  :  A  {}\mrightarrow{}  (corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)  \mtimes{}  bag(B))@i
11.  x  :  A  {}\mrightarrow{}  (corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)  \mtimes{}  bag(B))@i
12.  \mforall{}[inputs:A  List]
            (hdf-halted(inl  x1*(inputs))  =  hdf-halted(inl  x*(inputs))
            \mwedge{}  (\mforall{}[a:A].  (hdf-out(inl  x1*(inputs);a)  =  hdf-out(inl  x*(inputs);a))))@i
13.  ff  =  ff
14.  \mforall{}[a:A].  (hdf-out(inl  x1;a)  =  hdf-out(inl  x;a))
15.  a  :  A
\mvdash{}  (snd((x1  a)))  =  (snd((x  a)))


By

((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  RepUR  ``hdf-out  hdf-ap``  (-1)  THEN  Auto)\mcdot{}

---

Home Index