Nuprl Lemma : system-fpf_wf
[M:Type 
Type]. [S:System(P.M[P])].
(system-fpf(S) 
x:Id fp-> Process(P.M[P]) List 
LabeledGraph(pInTransit(P.M[P])))
Proof not projected
Definitions occuring in Statement :
system-fpf: system-fpf(S),
System: System(P.M[P]),
pInTransit: pInTransit(P.M[P]),
Process: Process(P.M[P]),
labeled-graph: LabeledGraph(T),
fpf: a:A fp-> B[a],
Id: Id,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type
Definitions :
implies: P 
Q,
all: x:A. B[x],
top: Top,
so_lambda: 
x.t[x],
mkfpf: mkfpf(a;b),
pi2: snd(t),
pi1: fst(t),
let: let,
system-fpf: system-fpf(S),
fpf: a:A fp-> B[a],
member: t T,
so_apply: x[s],
System: System(P.M[P]),
uall: [x:A]. B[x],
prop: 
,
ldag: LabeledDAG(T),
component: component(P.M[P]),
pInTransit: pInTransit(P.M[P])
Lemmas :
System_wf,
labeled-graph_wf,
l_member_wf,
pi2_wf,
pInTransit_wf,
lg-filter_wf,
top_wf,
assert_wf,
Process_wf,
eq_id_wf,
mapfilter_wf,
pi1_wf_top,
component_wf,
map_wf,
append_wf,
id-deq_wf,
Id_wf,
remove-repeats_wf
\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[S:System(P.M[P])].
(system-fpf(S) \mmember{} x:Id fp-> Process(P.M[P]) List \mtimes{} LabeledGraph(pInTransit(P.M[P])))
Date html generated:
2012_01_23-PM-12_41_56
Last ObjectModification:
2012_01_06-AM-10_23_55
Home
Index