{ 
[A:{A:
'| 
A} ]. [dfps:DataflowProgram(A) List]. [B:{B:Type|
valueall-type(B)} ].
[F:k:
||dfps|| 
bag(df-program-type(dfps[k])) bag(B)]. [L:A List].
last(data-stream(df-program-meaning(parallel-df-program-case1(B;F;dfps));L))
= (F (
k.last(data-stream(df-program-meaning(dfps[k]);L))))
supposing (0 < ||L||) 
((F (i.{})) = {}) }
{ Proof }
Definitions occuring in Statement :
parallel-df-program-case1: parallel-df-program-case1(B;F;dfps),
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
data-stream: data-stream(P;L),
select: l[i],
length: ||as||,
int_seg: {i..j
},
uimplies: b supposing a,
uall: [x:A]. B[x],
squash: T,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
list: type List,
natural_number: $n,
universe: Type,
equal: s = t,
last: last(L),
empty-bag: {},
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
corec: corec(T.F[T]),
listp: A List
,
combination: Combination(n;T),
true: True,
rev_implies: P 
Q,
iff: P 
Q,
minus: -n,
add: n + m,
top: Top,
nat: ,
sqequal: s ~ t,
pair: <a, b>,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
ge: i 
j ,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
dataflow: dataflow(A;B),
lelt: i 
j < k,
void: Void,
implies: P Q,
false: False,
not: 
A,
le: A B,
real: 
,
rationals: 
,
subtype: S T,
limited-type: LimitedType,
all: x:A. B[x],
empty-bag: {},
axiom: Ax,
apply: f a,
member: t 
T,
prop: 
,
squash: T,
valueall-type: valueall-type(T),
int_seg: {i..j},
uall: [x:A]. B[x],
so_lambda: 
x.t[x],
uimplies: b supposing a,
isect: 
x:A. B[x],
and: P Q,
product: x:A 
B[x],
less_than: a < b,
function: x:A B[x],
df-program-type: df-program-type(dfp),
dataflow-program: DataflowProgram(A),
set: {x:A| B[x]} ,
universe: Type,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
CollapseTHENA: Error :CollapseTHENA,
Complete: Error :Complete,
Try: Error :Try,
parallel-df-program-case1: parallel-df-program-case1(B;F;dfps),
df-program-meaning: df-program-meaning(dfp),
data-stream: data-stream(P;L),
lambda: x.A[x],
map: map(f;as),
select: l[i],
length: ||as||,
better-parallel-dataflow: better-parallel-dataflow,
bag: bag(T),
list: type List,
equal: s = t,
AssertBY: Error :AssertBY,
Unfold: Error :Unfold,
tactic: Error :tactic,
natural_number: $n,
subtract: n - m,
upto: upto(n),
last: last(L),
int: 
,
D: Error :D,
RepeatFor: Error :RepeatFor,
l_member: (x l),
assert: 
b,
proper-iseg: L1 < L2,
iseg: l1 l2,
l_exists: (
xL. P[x]),
multiply: n * m,
gt: i > j,
union: left + right,
or: P 
Q,
bool: 
,
null: null(as),
sq_type: SQType(T),
quotient: x,y:A//B[x; y],
fpf-sub: f g,
deq: EqDecider(T),
ma-state: State(ds),
fpf-dom: x dom(f),
guard: {T},
nil: [],
fpf-cap: f(x)?z
Lemmas :
int_seg_properties,
subtype_rel_list,
length-map,
null_wf3,
list_subtype_base,
subtype_base_sq,
length-map-sq,
length-data-stream,
non_null_iff_length,
pos-length,
equal-nil-sq-nil,
last-map,
assert_wf,
pos_length2,
uall_wf,
dataflow-program_wf,
valueall-type_wf,
int_seg_wf,
bag_wf,
df-program-type_wf,
select_wf,
squash_wf,
length_wf1,
empty-bag_wf,
parallel-df-program-case1-meaning,
parallel-df-program-case1_wf,
df-program-meaning_wf,
data-stream_wf,
last_wf,
length_upto,
length_wf_nat,
top_wf,
member_wf,
upto_wf,
iff_wf,
rev_implies_wf,
select_upto,
le_wf,
not_wf,
false_wf,
nat_wf,
dataflow_wf,
true_wf,
better-parallel-data-stream,
map_wf,
subtype_rel_wf,
select-map
\mforall{}[A:\{A:\mBbbU{}'| \mdownarrow{}A\} ]. \mforall{}[dfps:DataflowProgram(A) List]. \mforall{}[B:\{B:Type| valueall-type(B)\} ].
\mforall{}[F:k:\mBbbN{}||dfps|| {}\mrightarrow{} bag(df-program-type(dfps[k])) {}\mrightarrow{} bag(B)]. \mforall{}[L:A List].
last(data-stream(df-program-meaning(parallel-df-program-case1(B;F;dfps));L))
= (F (\mlambda{}k.last(data-stream(df-program-meaning(dfps[k]);L))))
supposing (0 < ||L||) \mwedge{} ((F (\mlambda{}i.\{\})) = \{\})
Date html generated:
2011_08_16-AM-09_39_31
Last ObjectModification:
2011_06_10-PM-05_12_39
Home
Index