Nuprl Lemma : hdf-state-single-val_wf

[A,B:Type]. ∀[X:hdataflow(A;B ⟶ B)]. ∀[b:B].
  (hdf-state-single-val(X;b) ∈ hdataflow(A;B)) supposing (hdf-single-valued(X;A;B ⟶ B) and valueall-type(B))


Definitions occuring in Statement :  hdf-state-single-val: hdf-state-single-val(X;b) hdf-single-valued: hdf-single-valued(X;A;B) hdataflow: hdataflow(A;B) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a hdf-state-single-val: hdf-state-single-val(X;b) prop: hdf-ap: X(a) subtype_rel: A ⊆B ext-eq: A ≡ B and: P ∧ Q all: x:A. B[x] implies:  Q ifthenelse: if then else fi  btrue: tt so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] hdf-run: hdf-run(P) hdf-single-valued: hdf-single-valued(X;A;B) iterate-hdataflow: P*(inputs) list_accum: list_accum nil: [] it: bool: 𝔹 unit: Unit uiff: uiff(P;Q) bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A callbyvalueall: callbyvalueall has-value: (a)↓ has-valueall: has-valueall(a) pi1: fst(t) top: Top nat: decidable: Dec(P) ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) hdf-halt: hdf-halt()

\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  B)].  \mforall{}[b:B].
    (hdf-state-single-val(X;b)  \mmember{}  hdataflow(A;B))  supposing 
          (hdf-single-valued(X;A;B  {}\mrightarrow{}  B)  and 

Date html generated: 2016_05_16-AM-10_40_31
Last ObjectModification: 2016_01_17-AM-11_13_28

Theory : halting!dataflow

Home Index