src/Sequents/Washing.thy
changeset 52446 473303ef6e34
parent 39406 0dec18004e75
child 56570 901a6696cdd8
equal deleted inserted replaced
52445:51e158e988a5 52446:473303ef6e34
     4 
     4 
     5 theory Washing
     5 theory Washing
     6 imports ILL
     6 imports ILL
     7 begin
     7 begin
     8 
     8 
     9 consts
     9 axiomatization
    10   dollar :: o
    10   dollar :: o and
    11   quarter :: o
    11   quarter :: o and
    12   loaded :: o
    12   loaded :: o and
    13   dirty :: o
    13   dirty :: o and
    14   wet :: o
    14   wet :: o and
    15   clean :: o
    15   clean :: o
    16 
    16 where
    17 axioms
       
    18   change:
    17   change:
    19   "dollar |- (quarter >< quarter >< quarter >< quarter)"
    18   "dollar |- (quarter >< quarter >< quarter >< quarter)" and
    20 
    19 
    21   load1:
    20   load1:
    22   "quarter , quarter , quarter , quarter , quarter |- loaded"
    21   "quarter , quarter , quarter , quarter , quarter |- loaded" and
    23 
    22 
    24   load2:
    23   load2:
    25   "dollar , quarter |- loaded"
    24   "dollar , quarter |- loaded" and
    26 
    25 
    27   wash:
    26   wash:
    28   "loaded , dirty |- wet"
    27   "loaded , dirty |- wet" and
    29 
    28 
    30   dry:
    29   dry:
    31   "wet, quarter , quarter , quarter |- clean"
    30   "wet, quarter , quarter , quarter |- clean"
    32 
    31 
    33 
    32