login  home  contents  what's new  discussion  bug reports     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
  
last edited 12 years ago by test1

Edit detail for #279 Equality fails for Set Any revision 1 of 3
1 2 3
Editor:
Time: 2007/11/17 22:20:23 GMT-8
Note: 
changed:
-
Equality of sets demands:
$$x \in X \iff x \in Y \implies X=Y$$

This axiom fails for the domain 'Set Any'. For example:
\begin{axiom}
X:Set Any
Y:Set Any
X:=["x"]
Y:=["x"]
(X=Y)::Boolean
\end{axiom}

and
\begin{axiom}
X:=[1.0]
Y:=[1.0]
(X=Y)::Boolean
\end{axiom}

But notice that the following cases work:
\begin{axiom}
X:=[1]
Y:=[1]
(X=Y)::Boolean
\end{axiom}

\begin{axiom}
Z:Set Union(String,Integer,Float)
W:Set Union(String,Integer,Float)
Z:=["x"]
W:=["x"]
(Z=W)::Boolean
\end{axiom}

Submitted by : (unknown) at: 2007-11-17T22:20:23-08:00 (18 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