{ 
[compList:(pi_prefix() 
Pi_term) List].
[g:{Q:Pi_term| (
C
compList. pi-rank(Q) 
pi-rank(snd(C)))}
Id
Name
Name List
pi-process()].
(pi-guarded-aux(compList;g) Id Name Name List pi-process()) }
{ Proof }
Definitions occuring in Statement :
pi-guarded-aux: pi-guarded-aux(compList;g),
pi-process: pi-process(),
pi-rank: pi-rank(p),
pi_term: Pi_term,
pi_prefix: pi_prefix(),
Id: Id,
name: Name,
uall: [x:A]. B[x],
pi2: snd(t),
le: A B,
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
product: x:A B[x],
list: type List,
l_exists: (xL. P[x])
Definitions :
uall: [x:A]. B[x],
member: t T,
pi-guarded-aux: pi-guarded-aux(compList;g),
top: Top,
ycomb: Y,
prop: 
,
so_lambda: 
x.t[x],
l_exists: (xL. P[x]),
le: A B,
pi2: snd(t),
pi-process: pi-process(),
ifthenelse: if b then t else f fi ,
let: let,
Process: Process(P.M[P]),
piM: piM(T),
process: process(P.M[P];P.E[P]),
corec: corec(T.F[T]),
uimplies: b supposing a,
isect2: T1 
T2,
btrue: tt,
bfalse: ff,
PiDataVal: PiDataVal(),
all: x:A. B[x],
implies: P 
Q,
and: P 
Q,
squash: 
T,
true: True,
not: 
A,
false: False,
exists: x:A. B[x],
cand: A c B,
int_seg: {i..j
},
lelt: i j < k,
type-monotone: Monotone(T.F[T]),
pMsg: pMsg(P.M[P]),
so_apply: x[s],
nat: 
,
bool: 
,
unit: Unit,
iff: P 
Q,
sq_stable: SqStable(P),
sq_type: SQType(T),
guard: {T},
it: 
Lemmas :
top_wf,
Id_wf,
pi_term_wf,
l_exists_wf,
pi_prefix_wf,
le_wf,
pi-rank_wf,
nat_wf,
pi2_wf,
l_member_wf,
name_wf,
pi-process_wf,
ycomb_wf_corec_3parameter,
piM_wf,
ldag_wf,
Com_wf,
continuous-constant,
strong-continuous-list,
pDVmsg?_wf,
bool_wf,
iff_weakening_uiff,
assert_wf,
eqtt_to_assert,
pDVmsg-val_wf,
pDVmsg-index_wf,
lt_int_wf,
nat_properties,
length_wf1,
uiff_transitivity,
assert_of_lt_int,
select_wf,
pircv?_wf,
pi-simple-subst_wf,
pircv-var_wf,
select_member,
l-union_wf,
name-deq_wf,
pi-names_wf,
Process_wf,
subtype_rel_transitivity,
make-lg_wf_dag,
mk-tagged_wf_pCom_msg,
sq_stable__subtype_rel,
pDVfire_wf,
not_wf,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
le_int_wf,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
pi-rank-pi-simple-subst,
subtype_base_sq,
int_subtype_base
\mforall{}[compList:(pi\_prefix() \mtimes{} Pi\_term) List]. \mforall{}[g:\{Q:Pi\_term|
(\mexists{}C\mmember{}compList. pi-rank(Q) \mleq{} pi-rank(snd(C)))\}
{}\mrightarrow{} Id
{}\mrightarrow{} Name
{}\mrightarrow{} Name List
{}\mrightarrow{} pi-process()].
(pi-guarded-aux(compList;g) \mmember{} Id {}\mrightarrow{} Name {}\mrightarrow{} Name List {}\mrightarrow{} pi-process())
Date html generated:
2011_08_17-PM-07_03_57
Last ObjectModification:
2011_06_18-PM-12_46_01
Home
Index