{ 
[S:Type]. [s0:S]. [n:
]. [M:Type 
Type].
[next:
m:
(S
M[m: 
if n 
z m then Top else lvprocess(lp.M[lp];m) fi ]
(S ((Id M[m:n lvprocess(lp.M[lp];m)]) List)))].
(RecProcess(s0;s,m.next[s;m]) 
lvprocess(lp.M[lp];n)) }
{ Proof }
Definitions occuring in Statement :
lvprocess: lvprocess(lp.M[lp];n),
rec-process: RecProcess(s0;s,m.next[s; m]),
Id: Id,
le_int: i z j,
ifthenelse: if b then t else f fi ,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
so_apply: x[s],
member: t T,
isect: x:A. B[x],
function: x:A B[x],
product: x:A B[x],
list: type List,
natural_number: $n,
universe: Type
Definitions :
prop: 
,
lelt: i j < k,
rationals: 
,
natural_number: $n,
int_seg: {i..j},
lambda: 
x.A[x],
top: Top,
real: 
,
grp_car: |g|,
subtype: S 
T,
le_int: i z j,
ifthenelse: if b then t else f fi ,
eclass: EClass(A[eo; e]),
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
ge: i 
j ,
less_than: a < b,
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A r B,
implies: P 
Q,
false: False,
not: 
A,
le: A B,
int: 
,
set: {x:A| B[x]} ,
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
process: process(P.M[P];P.E[P]),
Process: Process(P.M[P]),
uimplies: b supposing a,
all: x:A. B[x],
axiom: Ax,
so_apply: x[s1;s2],
rec-process: RecProcess(s0;s,m.next[s; m]),
lvprocess: lvprocess(lp.M[lp];n),
equal: s = t,
universe: Type,
uall: [x:A]. B[x],
member: t T,
isect: x:A. B[x],
function: x:A B[x],
list: type List,
product: x:A B[x],
Id: Id,
so_apply: x[s],
apply: f a,
nat: ,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic,
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
let: let,
Auto: Error :Auto,
Try: Error :Try
Lemmas :
rec-dataflow_wf,
member_wf,
ifthenelse_wf,
le_int_wf,
top_wf,
Id_wf,
int_seg_wf,
lvprocess_wf,
le_wf,
nat_wf
\mforall{}[S:Type]. \mforall{}[s0:S]. \mforall{}[n:\mBbbN{}]. \mforall{}[M:Type {}\mrightarrow{} Type].
\mforall{}[next:\mcap{}m:\mBbbN{}
(S
{}\mrightarrow{} M[m:\mBbbN{} \mtimes{} if n \mleq{}z m then Top else lvprocess(lp.M[lp];m) fi ]
{}\mrightarrow{} (S \mtimes{} ((Id \mtimes{} M[m:\mBbbN{}n \mtimes{} lvprocess(lp.M[lp];m)]) List)))].
(RecProcess(s0;s,m.next[s;m]) \mmember{} lvprocess(lp.M[lp];n))
Date html generated:
2011_08_17-PM-06_39_02
Last ObjectModification:
2011_06_18-PM-12_04_49
Home
Index