Nuprl Lemma : rec-dataflow-equiv

{

[A,B,S1,S2:Type].

[next1:S1

A

(S1

B)].

[next2:S2

A

(S2

B)].

[s1:S1].

[s2:S2].

[R:S1

S2

].
(rec-dataflow(s1;s,a.next1[s;a])

     rec-dataflow(s2;s,a.next2[s;a])) supposing
       (R[s1;s2] and
       (

s1:S1.

s2:S2.
(R[s1;s2]

(

a:A. R[fst(next1[s1;a]);fst(next2[s2;a])]))) and
(

s1:S1.

s2:S2.
(R[s1;s2]

(

a:A. ((snd(next1[s1;a])) = (snd(next2[s2;a]))))))) }

{ Proof }

Definitions occuring in Statement : dataflow-equiv: d1

d2, rec-dataflow: rec-dataflow(s0;s,m.next[s; m]), uimplies: b supposing a, uall:

[x:A]. B[x], prop:

, so_apply: x[s1;s2], pi1: fst(t), pi2: snd(t), all:

x:A. B[x], implies: P

Q, function: x:A

B[x], product: x:A

B[x], universe: Type, equal: s = t
Definitions : D: Error :D, RepeatFor: Error :RepeatFor, CollapseTHEN: Error :CollapseTHEN, Auto: Error :Auto, member: t

T, isect:

x:A. B[x], function: x:A

B[x], product: x:A

B[x], uall:

[x:A]. B[x], universe: Type, equal: s = t, all:

x:A. B[x], dataflow-equiv: d1

d2, uimplies: b supposing a, prop:

, implies: P

Q, so_apply: x[s1;s2], apply: f a, lambda:

x.A[x], list: type List, data-stream: data-stream(P;L), rec-dataflow: rec-dataflow(s0;s,m.next[s; m]), axiom: Ax, subtype_rel: A

r B, uiff: uiff(P;Q), and: P

Q, less_than: a < b, not:

A, ge: i

j , le: A

B, strong-subtype: strong-subtype(A;B), pi1: fst(t), top: Top, subtype: S

T, void: Void, limited-type: LimitedType, pi2: snd(t), so_lambda:

x.t[x], fpf: a:A fp-> B[a], pair: <a, b>, so_lambda:

x y.t[x; y], data_stream_nil: data_stream_nil{data_stream_nil_compseq_tag_def:o}(P), nil: [], cons: [car / cdr], hd: hd(l), tl: tl(l), sqequal: s ~ t, rec_dataflow_ap: rec_dataflow_ap_compseq_tag_def, dataflow-ap: df(a), RepUR: Error :RepUR, CollapseTHENA: Error :CollapseTHENA, BHyp: Error :BHyp
Lemmas : top_wf, member_wf, data-stream-cons, dataflow-equiv_wf, pi2_wf, pi1_wf_top

\mforall{}[A,B,S1,S2:Type]. \mforall{}[next1:S1 {}\mrightarrow{} A {}\mrightarrow{} (S1 \mtimes{} B)]. \mforall{}[next2:S2 {}\mrightarrow{} A {}\mrightarrow{} (S2 \mtimes{} B)]. \mforall{}[s1:S1]. \mforall{}[s2:S2]. \mforall{}[R:S1 {}\mrightarrow{} S2 {}\mrightarrow{} \mBbbP{}]. (rec-dataflow(s1;s,a.next1[s;a]) \mequiv{} rec-dataflow(s2;s,a.next2[s;a])) supposing (R[s1;s2] and (\mforall{}s1:S1. \mforall{}s2:S2. (R[s1;s2] {}\mRightarrow{} (\mforall{}a:A. R[fst(next1[s1;a]);fst(next2[s2;a])]))) and (\mforall{}s1:S1. \mforall{}s2:S2. (R[s1;s2] {}\mRightarrow{} (\mforall{}a:A. ((snd(next1[s1;a])) = (snd(next2[s2;a]))))))) Date html generated: 2011_08_10-AM-08_22_29 Last ObjectModification: 2010_12_30-PM-07_03_04 Home Index