[FN021] definition member_part_of

[fabianneuhaus]

@phismith
I propose the following definition of member_part_of

(cl:comment " x is a member_part_of y at t iff x is a member of a list ... such that
y is an ObjectAggregate of ... at t [FN021-001]")

(forall (x y t)
(iff
(member_part_of x y t)
(exists (...)
(and
(is_objectAggregate_of y ... t)
(oneOf x ...)))))

[phismith]

Do we then need a definition of 'list'?

On Mon, Sep 1, 2014 at 12:41 PM, fabianneuhaus notifications@github.com
wrote:

@phismith https://github.com/phismith
I propose the following definition of member_part_of

(cl:comment " x is a member_part_of y at t iff x is a member of a list ...
such that
y is an ObjectAggregate of ... at t [FN021-001]")

(forall (x y t)
(iff
(member_part_of x y t)
(exists (...)
(and
(is_objectAggregate_of y ... t)
(oneOf x ...)))))

—
Reply to this email directly or view it on GitHub
#71.

[fabianneuhaus]

No, I probably should have written "sequence". Quantification over
sequences are part of common logic. Below the symbol "..." is a sequence
variable.

Am 01/09/14 19:09, schrieb phismith:

Do we then need a definition of 'list'?

On Mon, Sep 1, 2014 at 12:41 PM, fabianneuhaus notifications@github.com
wrote:

@phismith https://github.com/phismith
I propose the following definition of member_part_of

(cl:comment " x is a member_part_of y at t iff x is a member of a
list ...
such that
y is an ObjectAggregate of ... at t [FN021-001]")

(forall (x y t)
(iff
(member_part_of x y t)
(exists (...)
(and
(is_objectAggregate_of y ... t)
(oneOf x ...)))))

—
Reply to this email directly or view it on GitHub
#71.

—
Reply to this email directly or view it on GitHub
#71 (comment).