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