Cross Reference: Simple_Implications.casl
xref: /ontohub/spec/fixtures/ontologies/prove/Simple_Implications.casl
  • Home
  • History
  • Annotate
  • Line#
  • Navigate
  • Download
  • only in ./
Simple_Implications.casl revision faffe37da53a86bab8f2e02c88f703ba1576e027
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaspec Group =
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa sort s
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa ops 0:s;
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa -__ :s->s;
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa __+__ :s*s->s, assoc
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa forall x,y:s
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . x+(-x) = 0
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . x+0=x %(leftunit)%
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . 0+x=x %(rightunit)% %implied
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . 0+0=0 %(zero_plus)% %implied
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaend
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaspec Empty =
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa sort t
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa forall x,y:t
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksa . x = x %implied
faffe37da53a86bab8f2e02c88f703ba1576e027Eugen Kuksaend

Indexes created Tue Jul 24 14:28:13 CEST 2018