@prefix : <#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .

this log:forAll :a , :b , :c , :d , :e , :f , :g , :h , :i , :j , :k , :l , :m , 
:n , :o , :p , :q , :r , :s , :t , :u , :v , :w , :x , :y , :z .

daml:equivalentTo 
   rdfs:domain rdfs:Resource; rdfs:range rdfs:Resource .
daml:sameClassAs rdfs:subPropertyOf 
   daml:equivalentTo, :equivInSetMembershipTo, rdfs:subClassOf; 
   rdfs:domain rdfs:Class; rdfs:range rdfs:Class .
daml:samePropertyAs rdfs:subPropertyOf 
   daml:equivalentTo, rdfs:subPropertyOf; 
   rdfs:domain rdf:Property; rdfs:range rdf:Property .
daml:sameIndividualAs rdfs:subPropertyOf daml:equivalentTo; 
   rdfs:domain daml:Thing; rdfs:range daml:Thing .
:equivInSetMembershipTo rdfs:subPropertyOf rdfs:subClassOf .
rdfs:subClassOf a daml:TransitiveProperty; 
   rdfs:domain rdfs:Class; rdfs:range rdfs:Class .

# "equivalentTo" stuff

{ :a daml:equivalentTo :b . :a :p :q } log:implies { :b :p :q } .
{ :a daml:equivalentTo :b . :p :a :q } log:implies { :p :b :q } .
{ :a daml:equivalentTo :b . :p :q :a } log:implies { :p :q :b } .

# "equivalentTo" is the inverse of itself

daml:equivalentTo a :ReversibleProperty .
:ReversibleProperty rdfs:subClassOf rdf:Property .
{ :y a :ReversibleProperty } log:implies { :y daml:inverseOf :y } .
{ :y daml:inverseOf :y . :x :y :z } log:implies { :z :y :x } .

# The usual implications of transitivity, and domain/ranges

daml:TransitiveProperty rdfs:subClassOf rdf:Property .
{ :x :y :z . :z :y :p . :y a daml:TransitiveProperty } 
   log:implies { :x :y :p } .

rdfs:range a rdf:Property; 
   rdfs:domain rdf:Property; rdfs:range rdfs:Class .
rdfs:domain a rdf:Property; 
   rdfs:domain rdf:Property; rdfs:range rdfs:Class .
rdfs:subPropertyOf rdfs:domain rdf:Property; rdfs:range rdf:Property .
rdfs:subClassOf rdfs:domain rdfs:Class; rdfs:range rdf:Class .
{ :x :y :z . :y rdfs:range :p } log:implies { :z a :p } .
{ :x :y :z . :y rdfs:domain :p } log:implies { :x a :p } .

# Set Membership Equivalence

{ :x a :y . :y :equivInSetMembershipTo :z } log:implies { :x a :z } .

# that basically follows from:-

{ :x a :y . :y rdfs:subClassOf :z } log:implies { :x a :z } .

# but *not*:-

{ :x a :y . :y daml:equivalentTo :z } log:implies { :x a :z } .

# although that *is* true.