---

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:

---

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


By

---

Latex:
((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