Nuprl Definition : prec-sub
prec-sub(P;lbl,p.a[lbl; p];j;x;i;y) ==
let lbl,z = dest-prec(y)
in let L = a[lbl; i] in
let n = ||L|| in
∃k:ℕn
((↑isl(L[k]))
∧ (((outl(L[k]) = (inl j) ∈ (P + P)) ∧ (x = z.k ∈ prec(lbl,i.a[lbl; i];j)))
∨ ((outl(L[k]) = (inr j ) ∈ (P + P)) ∧ (x ∈ z.k))))
Definitions occuring in Statement :
dest-prec: dest-prec(x),
prec: prec(lbl,p.a[lbl; p];i),
select-tuple: x.n,
l_member: (x ∈ l),
select: L[n],
length: ||as||,
int_seg: {i..j-},
outl: outl(x),
assert: ↑b,
isl: isl(x),
let: let,
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
spread: spread def,
inr: inr x ,
inl: inl x,
union: left + right,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
spread: spread def,
dest-prec: dest-prec(x),
let: let,
length: ||as||,
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
assert: ↑b,
isl: isl(x),
or: P ∨ Q,
inl: inl x,
and: P ∧ Q,
equal: s = t ∈ T,
union: left + right,
outl: outl(x),
select: L[n],
inr: inr x ,
l_member: (x ∈ l),
select-tuple: x.n,
prec: prec(lbl,p.a[lbl; p];i)
FDL editor aliases :
prec-sub
Latex:
prec-sub(P;lbl,p.a[lbl; p];j;x;i;y) ==
let lbl,z = dest-prec(y)
in let L = a[lbl; i] in
let n = ||L|| in
\mexists{}k:\mBbbN{}n
((\muparrow{}isl(L[k]))
\mwedge{} (((outl(L[k]) = (inl j)) \mwedge{} (x = z.k)) \mvee{} ((outl(L[k]) = (inr j )) \mwedge{} (x \mmember{} z.k))))
Date html generated:
2019_06_20-PM-02_05_36
Last ObjectModification:
2019_02_22-PM-06_33_21
Theory : tuples
Home
Index