Rewriting rules
introduction/elimination rules ts = s ;(i)=i
associativity (s1|(s2|s3)) = ((s1|s2)|s3) (i1;(i2;i3)) = ((i1;i2);i3)
pipe and sequential composition commute (i1;…;in) = (i1|…|in)
Previous slide
Next slide
Back to first slide
View graphic version