login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

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 


Submitted by : (unknown) at: 2007-11-17T22:20:23-08:00 (17 years ago)
Name :
Axiom Version :
Category : Severity : Status :
Optional subject :  
Optional comment :

Equality of sets demands:

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

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

fricas
(1) -> X:Set Any
Type: Void
fricas
Y:Set Any
Type: Void
fricas
X:=["x"]

\label{eq1}\left\{ \verb#"x"# \right\}(1)
Type: Set(Any)
fricas
Y:=["x"]

\label{eq2}\left\{ \verb#"x"# \right\}(2)
Type: Set(Any)
fricas
(X=Y)::Boolean

\label{eq3} \mbox{\rm true} (3)
Type: Boolean

and

fricas
X:=[1.0]

\label{eq4}\left\{{1.0}\right\}(4)
Type: Set(Any)
fricas
Y:=[1.0]

\label{eq5}\left\{{1.0}\right\}(5)
Type: Set(Any)
fricas
(X=Y)::Boolean

\label{eq6} \mbox{\rm true} (6)
Type: Boolean

But notice that the following cases work:

fricas
X:=[1]

\label{eq7}\left\{ 1 \right\}(7)
Type: Set(Any)
fricas
Y:=[1]

\label{eq8}\left\{ 1 \right\}(8)
Type: Set(Any)
fricas
(X=Y)::Boolean

\label{eq9} \mbox{\rm true} (9)
Type: Boolean

fricas
Z:Set Union(String,Integer,Float)
Type: Void
fricas
W:Set Union(String,Integer,Float)
Type: Void
fricas
Z:=["x"]

\label{eq10}\left\{ \verb#"x"# \right\}(10)
Type: Set(Union(String,Integer,Float))
fricas
W:=["x"]

\label{eq11}\left\{ \verb#"x"# \right\}(11)
Type: Set(Union(String,Integer,Float))
fricas
(Z=W)::Boolean

\label{eq12} \mbox{\rm true} (12)
Type: Boolean

Category: Axiom Mathematics => Axiom Library

Status: open => closed