{ 
[P:Pi_term]. [t,x:Name]. [avoid:Name List].
(pi-rank(pi-simple-subst-aux(t;x;P;avoid)) = pi-rank(P)) }
{ Proof }
Definitions occuring in Statement :
pi-simple-subst-aux: pi-simple-subst-aux(t;x;P;avoid),
pi-rank: pi-rank(p),
pi_term: Pi_term,
name: Name,
uall: [x:A]. B[x],
list: type List,
int: 
,
equal: s = t
Definitions :
assert: 
b,
eclass: EClass(A[eo; e]),
pair: <a, b>,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
product: x:A 
B[x],
and: P 
Q,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
isect: 
x:A. B[x],
axiom: Ax,
pi-simple-subst-aux: pi-simple-subst-aux(t;x;P;avoid),
pi-rank: pi-rank(p),
int: ,
list: type List,
rec: rec(x.A[x]),
pi_term: Pi_term,
all: x:A. B[x],
function: x:A 
B[x],
uall: [x:A]. B[x],
equal: s = t,
name: Name,
member: t 
T,
tactic: Error :tactic,
guard: {T},
limited-type: LimitedType,
false: False,
true: True,
squash: 
T,
set: {x:A| B[x]} ,
real: 
,
grp_car: |g|,
subtype: S T,
natural_number: $n,
prop: 
,
universe: Type,
minus: -n,
add: n + m,
subtract: n - m,
void: Void,
lambda: 
x.A[x],
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
implies: P 
Q,
AssertBY: Error :AssertBY,
Try: Error :Try,
nat: 
,
pinew: (new name. body),
pi_term_ind_pinew: pi_term_ind_pinew_compseq_tag_def,
pi_term_ind_pirep: pi_term_ind_pirep_compseq_tag_def,
pi_term_ind_pipar: pi_term_ind_pipar_compseq_tag_def,
rev_implies: P 
Q,
iff: P Q,
pi_term_ind_pioption: pi_term_ind_pioption_compseq_tag_def,
maybe-new: maybe-new(s;avoid),
pi-replace: pi-replace(t;x;P),
cons: [car / cdr],
pircv: chan?(var),
name_eq: name_eq(x;y),
ifthenelse: if b then t else f fi ,
pisend: chan<val>,
picomm: pre.body,
let: let,
pi_prefix_ind: pi_prefix_ind,
pi_term_ind_picomm: pi_term_ind_picomm_compseq_tag_def,
p-outcome: Outcome,
rationals: 
,
apply: f a,
pi_term_ind_pizero: pi_term_ind_pizero_compseq_tag_def,
pi_prefix: pi_prefix(),
union: left + right,
unit: Unit,
pircv-chan: pircv-chan(x),
pi_prefix_ind_pircv: pi_prefix_ind_pircv_compseq_tag_def,
pircv-var: pircv-var(x),
pisend?: pisend?(x),
pircv?: pircv?(x),
pisend-chan: pisend-chan(x),
pi_prefix_ind_pisend: pi_prefix_ind_pisend_compseq_tag_def,
pisend-val: pisend-val(x),
l_member: (x l),
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
Unfold: Error :Unfold,
RepUR: Error :RepUR,
tl: tl(l),
hd: hd(l),
pizero?: pizero?(x),
picomm?: picomm?(x),
pioption?: pioption?(x),
pipar?: pipar?(x),
pirep?: pirep?(x),
pinew?: pinew?(x),
pinew-name: pinew-name(x),
pinew-body: pinew-body(x)
Lemmas :
pi_prefix_wf,
l_member_wf,
maybe-new_wf,
pi-replace_wf,
pircv_wf,
picomm_wf,
name_eq_wf,
ifthenelse_wf,
pisend_wf,
pi_prefix_ind_wf,
pi_prefix-induction,
pi-rank-pi-replace,
false_wf,
not_wf,
member_wf,
iff_wf,
rev_implies_wf,
add_functionality_wrt_eq,
pi-simple-subst-aux_wf,
ge_wf,
nat_properties,
nat_ind_tp,
comp_nat_ind_tp,
le_wf,
nat_wf,
pi_term_wf,
name_wf,
pi-rank_wf
\mforall{}[P:Pi\_term]. \mforall{}[t,x:Name]. \mforall{}[avoid:Name List].
(pi-rank(pi-simple-subst-aux(t;x;P;avoid)) = pi-rank(P))
Date html generated:
2011_08_17-PM-06_50_19
Last ObjectModification:
2011_06_18-PM-12_23_38
Home
Index