Nuprl Definition : list-match
list-match(L1;L2;a,b.R[a; b]) == ∃f:ℕ||L1|| ⟶ ℕ||L2|| [(Inj(ℕ||L1||;ℕ||L2||;f) ∧ (∀i:ℕ||L1||. R[L1[i]; L2[f i]]))]
Definitions occuring in Statement :
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]],
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
sq_exists: ∃x:A [B[x]],
function: x:A ⟶ B[x],
and: P ∧ Q,
inject: Inj(A;B;f),
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
select: L[n],
apply: f a
FDL editor aliases :
list-match
Latex:
list-match(L1;L2;a,b.R[a; b]) ==
\mexists{}f:\mBbbN{}||L1|| {}\mrightarrow{} \mBbbN{}||L2|| [(Inj(\mBbbN{}||L1||;\mBbbN{}||L2||;f) \mwedge{} (\mforall{}i:\mBbbN{}||L1||. R[L1[i]; L2[f i]]))]
Date html generated:
2018_05_21-PM-00_45_40
Last ObjectModification:
2018_01_17-PM-05_39_37
Theory : list_1
Home
Index