***************** SmallKB/qq.maude  ***************** 

mod QQ is
inc ALLRULES .
inc MODEL-CHECKER .

subsort Dish < State .


ops rasDish rafUbe213Dish : -> Dish .
eq rasDish =  
  PD( 
     {XOut | Egf}
     {CLm | EgfR  PIP2 }
     {CLi | [Hras - GDP]  Src }
     {CLc | Gab1 Grb2 Pi3k Plcg Sos1 } ) .


eq rafUbe213Dish =  
  PD( 
     {XOut | Egf}
     {CLm | EgfR  PIP2 }
     {CLi | [Hras - GDP]  Src [Ube2l3 - ubiq]}
     {CLc | Cbl Gab1 Grb2 Pi3k Plcg  Sos1 1433x1 Pak1  Raf1 PP2a } 
 ) .

ops tgfaDish : -> Dish .
eq tgfaDish =  
  PD( 
     {XOut | Tgfa}
     {CLm | EgfR  PIP2 }
     {CLi | [Hras - GDP]  Src [Ube2l3 - ubiq]}
     {CLc | Cbl Gab1 Grb2 Pi3k Plcg  Sos1 1433x1 Pak1  Raf1 PP2a } 
 ) .

***(
op allDish : -> Dish .
eq allDish =
   PD(
      {XOut | Egf Tgfa }
      {CLm | EgfR  PIP2 }
      {CLi | [Hras - GDP]  Src [Ube2l3 - ubiq]}
      {CLc | Cbl Gab1 Grb2 Pi3k Plcg  Sos1 1433x1 Pak1  Raf1 PP2a } 
 ) .
)

endm

