help links subscribe changes refresh edit

	IssueTracker
#278 'simplifyLog' cannot cope with 'sqrt' ←	↑	→ #28 GCL 2.6.5 on FC3

#279 Equality fails for Set Any

Edit detail for #279 Equality fails for Set Any revision 3 of 3

	1 2 3
Editor: test1 Time: 2014/04/23 18:54:02 GMT+0
Note:

added:

From test1 Wed Apr 23 18:54:02 +0000 2014
From: test1
Date: Wed, 23 Apr 2014 18:54:02 +0000
Subject: 
Message-ID: <20140423185402+0000@axiom-wiki.newsynthesis.org>

Status: open => closed

Equality of sets demands:

$x \in X \iff x \in Y \implies X=Y$

This axiom fails for the domain Set Any. For example:

axiom

X:Set Any

Type: Void

axiom

Y:Set Any

Type: Void

axiom

X:=["x"]

$\label{eq1}\left\{ \mbox{\tt "x"}\right\}$

(1)

Type: Set(Any)

axiom

Y:=["x"]

$\label{eq2}\left\{ \mbox{\tt "x"}\right\}$

(2)

Type: Set(Any)

axiom

(X=Y)::Boolean

$\label{eq3} \mbox{\rm true}$

(3)

Type: Boolean

and

axiom

X:=[1.0]

$\label{eq4}\left\{{1.0}\right\}$

(4)

Type: Set(Any)

axiom

Y:=[1.0]

$\label{eq5}\left\{{1.0}\right\}$

(5)

Type: Set(Any)

axiom

(X=Y)::Boolean

$\label{eq6} \mbox{\rm true}$

(6)

Type: Boolean

But notice that the following cases work:

axiom

X:=[1]

$\label{eq7}\left\{ 1 \right\}$

(7)

Type: Set(Any)

axiom

Y:=[1]

$\label{eq8}\left\{ 1 \right\}$

(8)

Type: Set(Any)

axiom

(X=Y)::Boolean

$\label{eq9} \mbox{\rm true}$

(9)

Type: Boolean

axiom

Z:Set Union(String,Integer,Float)

Type: Void

axiom

W:Set Union(String,Integer,Float)

Type: Void

axiom

Z:=["x"]

$\label{eq10}\left\{ \mbox{\tt "x"}\right\}$

(10)

Type: Set(Union(String,Integer,Float))

axiom

W:=["x"]

$\label{eq11}\left\{ \mbox{\tt "x"}\right\}$

(11)

Type: Set(Union(String,Integer,Float))

axiom

(Z=W)::Boolean

$\label{eq12} \mbox{\rm true}$

(12)

Type: Boolean

... --kratt6, Fri, 28 Dec 2007 14:20:21 -0800 reply

Category: Axiom Mathematics => Axiom Library

... --test1, Wed, 23 Apr 2014 18:54:02 +0000 reply

Status: open => closed