---

Step * of Lemma hdf-ap_wf

∀[A,B:Type]. ∀[X:hdataflow(A;B)]. ∀[a:A].  (X(a) ∈ hdataflow(A;B) × bag(B))
BY
{ ((Auto THEN (InstLemma `hdataflow-ext` [⌈A⌉;⌈B⌉]⋅ THENA Auto))
   THEN (GenConcl ⌈X = F ∈ (A ─→ (hdataflow(A;B) × bag(B))?)⌉⋅ THENA (Auto THEN DoSubsume⋅ THEN Auto))
   THEN ThinVar `X'
   THEN ProveWfLemma
   THEN SubsumeC ⌈A ─→ (hdataflow(A;B) × bag(B))?⌉⋅
   THEN Auto) }

---

Latex:


\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[a:A].    (X(a)  \mmember{}  hdataflow(A;B)  \mtimes{}  bag(B))


By

((Auto  THEN  (InstLemma  `hdataflow-ext`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}X  =  F\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  DoSubsume\mcdot{}  THEN  Auto))
  THEN  ThinVar  `X'
  THEN  ProveWfLemma
  THEN  SubsumeC  \mkleeneopen{}A  {}\mrightarrow{}  (hdataflow(A;B)  \mtimes{}  bag(B))?\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index