Nuprl 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)))))
Proof
Definitions occuring in Statement :
iterate-hdataflow: P*(inputs),
hdf-out: hdf-out(P;x),
hdf-halted: hdf-halted(P),
hdataflow: hdataflow(A;B),
list: T List,
bool: 𝔹,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T,
bag: bag(T)
Lemmas :
iff_imp_equal_bool,
hdf-halted_wf,
iterate-hdataflow_wf,
and_wf,
equal_wf,
hdataflow_wf,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_wf,
hdf-out_wf,
list_wf,
coinduction-principle,
bag_wf,
unit_wf2,
continuous-monotone-union,
continuous-monotone-function,
continuous-monotone-product,
continuous-monotone-id,
continuous-monotone-constant,
uall_wf,
corec_wf,
corec_subtype,
strong-continuous-union,
strong-continuous-function,
strong-continuous-product,
continuous-id,
continuous-constant,
subtype_rel_weakening,
nat_wf,
subtype_corec,
subtype_rel_sum,
subtype_rel_function,
subtype_rel_simple_product,
subtype_rel_wf,
all_wf,
nil_wf,
iter_hdf_nil_lemma,
pair-eta,
subtype_rel_product,
top_wf,
subtype_top,
btrue_neq_bfalse,
equal-unit,
cons_wf,
iter_hdf_cons_lemma,
iff_weakening_equal
\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)))))
Date html generated:
2015_07_17-AM-08_05_09
Last ObjectModification:
2015_02_03-PM-09_46_37
Home
Index