---

Step * 1 1 of Lemma hdataflow-equal

.....subterm..... T:t
1: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
⊢ (fst((x1 a))) = (fst((x a))) ∈ P1
BY
{ ((BackThruSomeHyp THEN Auto)
   THEN OnMaybeHyp 12 (\h. ((InstHyp [⌈[a / inputs]⌉] h⋅ THENA Auto)
                            THEN Reduce (-1)
                            THEN RepUR ``hdf-ap`` (-1)
                            THEN Complete (Auto))⋅)
   )⋅ }

---

Latex:


.....subterm.....  T:t
1: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{}  (fst((x1  a)))  =  (fst((x  a)))


By

((BackThruSomeHyp  THEN  Auto)
  THEN  OnMaybeHyp  12  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}[a  /  inputs]\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                                    THEN  Reduce  (-1)
                                                    THEN  RepUR  ``hdf-ap``  (-1)
                                                    THEN  Complete  (Auto))\mcdot{})
  )\mcdot{}

---

Home Index