80                   apply (rule injI, simp)

    80                   apply (rule injI, simp)

    81                   by (unfold image_comp, simp)

    81                   by (unfold image_comp, simp)

    82   have [simp]: "preceds {th} s = {the_preced s th}"

    82   have [simp]: "preceds {th} s = {the_preced s th}"

    83     by (unfold the_preced_def, simp)

    83     by (unfold the_preced_def, simp)

    84   show ?thesis 

    84   show ?thesis 

    86 qed    

    90 qed    

    87 

    91 

    88 text {*

    92 text {*

    89   According to this lemma, @{text cp}-value of one thread can be calculated by calling recursively 

    93   According to this lemma, @{text cp}-value of one thread can be calculated by calling recursively 

    90   the @{text cp} function on its @{text tG}-children. However, one thing to be noted is that

    94   the @{text cp} function on its @{text tG}-children. However, one thing to be noted is that

   961 text {*

   965 text {*

   962   Now, since @{term th} has no children, by definition its @{text cp} value 

   966   Now, since @{term th} has no children, by definition its @{text cp} value 

   963   equals its precedence:

   967   equals its precedence:

   964 *}

   968 *}

   965 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"

   969 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"

   968 end

   975 end

   969 

   976 

   970 text {*

   977 text {*

   971   The following locale @{text valid_trace_exit} deals with the @{term Exit}-operation.

   978   The following locale @{text valid_trace_exit} deals with the @{term Exit}-operation.

   972 *}

   979 *}