___________________________________________ | T || x | sf | fr | rb | bs | y | |____||_____|_____|_____|_____|_____|_____| ___________________________________________ | 0 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 1 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 2 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 3 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 4 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 5 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 6 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 7 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 8 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 9 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 10 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 11 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 12 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 13 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 14 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 15 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 16 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 17 || | | | | | | |____||_____|_____|_____|_____|_____|_____| | 18 || | | | | | | |____||_____|_____|_____|_____|_____|_____| ___________________________________________ | T || x | sf | fr | rb | bs | y | |____||_____|_____|_____|_____|_____|_____|
_______________________________________________________ | T || x | sf.v| sf.t| fr.v| fr.t| rb | bs | y | |____||_____|_____|_____|_____|_____|_____|_____|_____| _______________________________________________________ | 0 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 1 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 2 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 3 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 4 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 5 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 6 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 7 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 8 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 9 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 10 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 11 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 12 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 13 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 14 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 15 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 16 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 17 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 18 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| | 19 || | | | | | | | | |____||_____|_____|_____|_____|_____|_____|_____|_____| _______________________________________________________ | T || x | sf.v| sf.t| fr.v| fr.t| rb | bs | y | |____||_____|_____|_____|_____|_____|_____|_____|_____|
_____________________________________________________________ | S = proc (x?Msg & sf!TMsg & bs?Msg). | |___________________________________________________________| | begin m: var TMsg & a: var Msg | |___________________________________________________________| | | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | end | |___________________________________________________________|
_____________________________________________________________ | R = proc (fr?TMsg & rb!Msg & y!Msg). | |___________________________________________________________| | begin m: var TMsg & u: var Nat | |___________________________________________________________| | | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | | |___________________________________________________________| | end | |___________________________________________________________|