### 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