Nuprl Definition : rel_path
rel_path(A;L;x;y) ==
rec-case(L) of [] => λx,y. (x = y ∈ A) | a::as => rec.λx,y. (((fst(a)) = x ∈ A) ∧ (rec (fst(snd(a))) y)) x y
Definitions occuring in Statement :
list_ind: list_ind,
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
list_ind: list_ind,
lambda: λx.A[x],
and: P ∧ Q,
equal: s = t ∈ T,
apply: f a,
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
rel_path
Latex:
rel\_path(A;L;x;y) ==
rec-case(L) of [] => \mlambda{}x,y. (x = y) | a::as => rec.\mlambda{}x,y. (((fst(a)) = x) \mwedge{} (rec (fst(snd(a))) y)) x\000C y
Date html generated:
2016_05_14-PM-03_51_03
Last ObjectModification:
2015_09_22-PM-06_01_45
Theory : relations2
Home
Index