---

Step * of Lemma hdataflow-equal

∀[A,B:Type]. ∀[P,Q:hdataflow(A;B)].
  uiff(P = Q ∈ hdataflow(A;B);∀[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)))))
BY
{ (Auto
   THEN All (Unfold `hdataflow`)
   THEN Using [`R',⌈λ2P Q.∀[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))))⌉
   ] (BLemma `coinduction-principle`)⋅
   THEN Auto
   THEN Try ((All (Fold `hdataflow`) THEN Complete (Auto)))
   THEN Auto
   THEN D 0
   THEN Auto
   THEN (DCorecVar `x' THENA Auto)
   THEN Try (Complete (Auto))
   THEN (DCorecVar `y' THENA Auto)
   THEN Try (Complete (Auto))
   THEN (D 0
         THENA (Assert ⌈(x ∈ hdataflow(A;B)) ∧ (y ∈ hdataflow(A;B))⌉⋅
                THEN Auto
                THEN (InstLemma `subtype_corec` [⌈λ2P.A ─→ (P × bag(B))?⌉]⋅ THENA Auto)
                THEN Unfold `hdataflow` 0
                THEN DoSubsume
                THEN Auto)
         )) }

1
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. x : A ─→ (corec(P.A ─→ (P × bag(B))?) × bag(B))?@i
11. y : A ─→ (corec(P.A ─→ (P × bag(B))?) × bag(B))?@i
12. ∀[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))))@i
⊢ x = y ∈ (A ─→ (P1 × bag(B))?)

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[P,Q:hdataflow(A;B)].
    uiff(P  =  Q;\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)))))


By

(Auto
  THEN  All  (Unfold  `hdataflow`)
  THEN  Using  [`R',\mkleeneopen{}\mlambda{}\msubtwo{}P  Q.\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))))\mkleeneclose{}
  ]  (BLemma  `coinduction-principle`)\mcdot{}
  THEN  Auto
  THEN  Try  ((All  (Fold  `hdataflow`)  THEN  Complete  (Auto)))
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  (DCorecVar  `x'  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  (DCorecVar  `y'  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  (D  0
              THENA  (Assert  \mkleeneopen{}(x  \mmember{}  hdataflow(A;B))  \mwedge{}  (y  \mmember{}  hdataflow(A;B))\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  (InstLemma  `subtype\_corec`  [\mkleeneopen{}\mlambda{}\msubtwo{}P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  Unfold  `hdataflow`  0
                            THEN  DoSubsume
                            THEN  Auto)
              ))

---

Home Index