Nuprl Definition : agree_on_common
agree_on_common(T;as;bs) ==
fix((λagree_on_common,as,bs. case as of
[] => True
a::as' =>
case bs of
[] => True
b::bs' =>
((¬(a ∈ bs)) ∧ (agree_on_common as' bs))
∨ ((¬(b ∈ as)) ∧ (agree_on_common as bs'))
∨ ((a = b ∈ T) ∧ (agree_on_common as' bs'))
esac
esac))
as
bs
Definitions occuring in Statement :
l_member: (x ∈ l),
list_ind: list_ind,
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
true: True,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
list_ind: list_ind,
true: True,
or: P ∨ Q,
not: ¬A,
l_member: (x ∈ l),
and: P ∧ Q,
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
agree_on_common
Latex:
agree\_on\_common(T;as;bs) ==
fix((\mlambda{}agree\_on$_{common}$,as,bs. case as of
[] => True
a::as' =>
case bs of
[] => True
b::bs' =>
((\mneg{}(a \mmember{} bs)) \mwedge{} (agree\_on$_{common}$ as' bs))
\mvee{} ((\mneg{}(b \mmember{} as)) \mwedge{} (agree\_on$_{common}$ as bs')\000C)
\mvee{} ((a = b) \mwedge{} (agree\_on$_{common}$ as' bs'))
esac
esac))
as
bs
Date html generated:
2016_05_15-PM-01_53_14
Last ObjectModification:
2015_09_23-AM-07_37_22
Theory : list!
Home
Index