---

Step * 1 of Lemma hdataflow-equal


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))?)
BY
{ ((InstHyp [⌈[]⌉] (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN DVar `x'
   THEN DVar `y'
   THEN RepUR ``hdf-halted`` (-1)
   THEN Auto
   THEN (Auto
         THEN Ext
         THEN Auto
         THEN Try ((DoSubsume THEN Auto))
         THEN RenameVar `a' (-1)
         THEN (RW (AddrC [2] (LemmaC `pair-eta`)) 0 THENA Auto)
         THEN (RW (AddrC [3] (LemmaC `pair-eta`)) 0 THENA Auto)
         THEN EqCD)⋅) }

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

2
.....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)

---

Latex:



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.  x  :  A  {}\mrightarrow{}  (corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)  \mtimes{}  bag(B))?@i
11.  y  :  A  {}\mrightarrow{}  (corec(P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)  \mtimes{}  bag(B))?@i
12.  \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))))@i
\mvdash{}  x  =  y


By

((InstHyp  [\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  RepUR  ``hdf-halted``  (-1)
  THEN  Auto
  THEN  (Auto
              THEN  Ext
              THEN  Auto
              THEN  Try  ((DoSubsume  THEN  Auto))
              THEN  RenameVar  `a'  (-1)
              THEN  (RW  (AddrC  [2]  (LemmaC  `pair-eta`))  0  THENA  Auto)
              THEN  (RW  (AddrC  [3]  (LemmaC  `pair-eta`))  0  THENA  Auto)
              THEN  EqCD)\mcdot{})

---

Home Index