CTX_sysMethod_Split : CONTEXT =
BEGIN
  
  STATE : TYPE =
    [# inst_rg1 : CTX_RegUN{8}!STATE
     , inst_rg2 : CTX_RegUN{8}!STATE
     , inst_c : CTX_RegUN{1}!STATE
     #] ;
  
  ctor : STATE =
    (# inst_rg1 := CTX_RegUN{8}!ctor
     , inst_rg2 := CTX_RegUN{8}!ctor
     , inst_c := CTX_RegUN{1}!ctor
     #) ;
  
  meth_m (state0 : STATE) : [ STATE, Bit{8}!T ] =
    LET def_c__h135 : Bit{1}!T = CTX_RegUN{1}!meth_read(state0.inst_c)
    IN IF Prim!bitToBool(def_c__h135)
	 THEN LET def_x__h213 : Bit{8}!T = CTX_RegUN{8}!meth_read(state0.inst_rg1)
	      IN LET def_x__h218 : Bit{8}!T = CTX_RegUN{8}!meth_read(state0.inst_rg2)
	      IN LET def_y_avValue__h212 : Bit{8}!T = Prim1{8}!primAdd(def_x__h213, Bit{8}!mkConst(1))
	      IN LET def_y_avValue__h217 : Bit{8}!T = Prim1{8}!primAdd(def_x__h218, Bit{8}!mkConst(2))
	      IN LET def_x__h155 : Bit{8}!T = Prim1{8}!primAdd(def_x__h213, Bit{8}!mkConst(3))
	      IN LET act1 : [ CTX_RegUN{8}!STATE, Unit!T ] = CTX_RegUN{8}!meth_write(def_x__h155, state0.inst_rg1)
	      IN LET state1 : STATE = state0 WITH .inst_rg1 := act1.1
	      IN ( state1,
		   IF Prim!bitToBool(def_c__h135) THEN def_y_avValue__h212 ELSE def_y_avValue__h217 ENDIF )
	 ELSE IF (NOT Prim!bitToBool(def_c__h135))
		THEN LET def_x__h213 : Bit{8}!T = CTX_RegUN{8}!meth_read(state0.inst_rg1)
		     IN LET def_x__h218 : Bit{8}!T = CTX_RegUN{8}!meth_read(state0.inst_rg2)
		     IN LET def_y_avValue__h212 : Bit{8}!T = Prim1{8}!primAdd(def_x__h213, Bit{8}!mkConst(1))
		     IN LET def_y_avValue__h217 : Bit{8}!T = Prim1{8}!primAdd(def_x__h218, Bit{8}!mkConst(2))
		     IN LET def_x__h193 : Bit{8}!T = Prim1{8}!primAdd(def_x__h218, Bit{8}!mkConst(4))
		     IN LET act1 : [ CTX_RegUN{8}!STATE, Unit!T ] =
			      CTX_RegUN{8}!meth_write(def_x__h193, state0.inst_rg2)
		     IN LET state1 : STATE = state0 WITH .inst_rg2 := act1.1
		     IN ( state1,
			  IF Prim!bitToBool(def_c__h135) THEN def_y_avValue__h212 ELSE def_y_avValue__h217 ENDIF )
		ELSE LET def_x__h213 : Bit{8}!T = CTX_RegUN{8}!meth_read(state0.inst_rg1)
		     IN LET def_x__h218 : Bit{8}!T = CTX_RegUN{8}!meth_read(state0.inst_rg2)
		     IN LET def_y_avValue__h212 : Bit{8}!T = Prim1{8}!primAdd(def_x__h213, Bit{8}!mkConst(1))
		     IN LET def_y_avValue__h217 : Bit{8}!T = Prim1{8}!primAdd(def_x__h218, Bit{8}!mkConst(2))
		     IN ( state0,
			  IF Prim!bitToBool(def_c__h135) THEN def_y_avValue__h212 ELSE def_y_avValue__h217 ENDIF )
	      ENDIF
       ENDIF ;
  
  meth_RDY_m (state0 : STATE) : BOOLEAN = TRUE ;
  
END