{ 
[q:(Id 
(pi_prefix() List)) List]
(Comm-process-q_aux(q) 
Id
st:Id fp-> pi_prefix() List
((Id (pi_prefix() List)) List
st:Id fp-> pi_prefix() List
Id
((
Id Name) List))) }
{ Proof }
Definitions occuring in Statement :
Comm-process-q_aux: Comm-process-q_aux(q),
pi_prefix: pi_prefix(),
fpf: a:A fp-> B[a],
Id: Id,
name: Name,
nat: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List
Definitions :
eclass: EClass(A[eo; e]),
strong-subtype: strong-subtype(A;B),
atom: Atom$n,
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
pi1: fst(t),
pi2: snd(t),
get-triples: get-triples(preList;st),
fpf-single: x : v,
id-deq: IdDeq,
fpf-join: f 
g,
null: null(as),
ifthenelse: if b then t else f fi ,
apply: f a,
let: let,
list_ind: list_ind def,
nil: [],
pair: <a, b>,
lambda: 
x.A[x],
all: x:A. B[x],
axiom: Ax,
Comm-process-q_aux: Comm-process-q_aux(q),
equal: s = t,
name: Name,
nat: ,
fpf: a:A fp-> B[a],
so_lambda: 
x.t[x],
prop: 
,
universe: Type,
list: type List,
pi_prefix: pi_prefix(),
Id: Id,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
Auto: Error :Auto,
THEN: Error :THEN,
void: Void,
fpf-cap: f(x)?z,
subtype: S T,
top: Top,
RepUR: Error :RepUR,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic
Lemmas :
top_wf,
pi1_wf_top,
fpf-single_wf,
fpf-join_wf,
pi2_wf,
null_wf3,
id-deq_wf,
nat_wf,
name_wf,
ifthenelse_wf,
Id_wf,
pi_prefix_wf,
fpf_wf,
get-triples_wf,
pi1_wf,
member_wf,
uall_wf
\mforall{}[q:(Id \mtimes{} (pi\_prefix() List)) List]
(Comm-process-q\_aux(q) \mmember{} Id
{}\mrightarrow{} st:Id fp-> pi\_prefix() List
{}\mrightarrow{} ((Id \mtimes{} (pi\_prefix() List)) List
\mtimes{} st:Id fp-> pi\_prefix() List
\mtimes{} Id
\mtimes{} ((\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name) List)))
Date html generated:
2011_08_17-PM-07_02_18
Last ObjectModification:
2011_06_18-PM-12_42_59
Home
Index