UFMG - Pós-graduação em Ciência da Computação - Programação Paralela

A seguir: Theorem 1: ``Proof'' for Acima: Progress: the Graph Anterior: Theorem 1: Initial Conditions

Theorem 1: Scanning the Rules

• Now we will show that for every rule R, if A2 $\wedge$ A3 $\wedge$ A4 $\wedge$ A5 and the enabling predicate hold, then Theorem 1 will hold after the rule's action.
• Rules 1 to 3 do not change relation , so they trivially verify the induction step.
• The following conventions are used to represent graphically the graph: