### Nuprl Definition : list-match-aux

`list-match-aux(L1;L2;used;a,b.R[a; b]) ==`
`  ∃f:ℕ||L1|| ⟶ ℕ||L2|| [(Inj(ℕ||L1||;ℕ||L2||;f) ∧ (∀i:ℕ||L1||. ((¬(f i ∈ used)) ∧ R[L1[i]; L2[f i]])))]`

Definitions occuring in Statement :  l_member: `(x ∈ l)` select: `L[n]` length: `||as||` inject: `Inj(A;B;f)` int_seg: `{i..j-}` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` not: `¬A` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ`
Definitions occuring in definition :  sq_exists: `∃x:A [B[x]]` function: `x:A ⟶ B[x]` inject: `Inj(A;B;f)` all: `∀x:A. B[x]` int_seg: `{i..j-}` natural_number: `\$n` length: `||as||` and: `P ∧ Q` not: `¬A` l_member: `(x ∈ l)` int: `ℤ` select: `L[n]` apply: `f a`
FDL editor aliases :  list-match-aux

Latex:
list-match-aux(L1;L2;used;a,b.R[a;  b])  ==
\mexists{}f:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L2||  [(Inj(\mBbbN{}||L1||;\mBbbN{}||L2||;f)
\mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  ((\mneg{}(f  i  \mmember{}  used))  \mwedge{}  R[L1[i];  L2[f  i]])))]

Date html generated: 2018_05_21-PM-00_46_17
Last ObjectModification: 2018_01_17-PM-05_40_59

Theory : list_1

Home Index