equal
deleted
inserted
replaced
99 apply (rule_tac [2] zg.Nil |
99 apply (rule_tac [2] zg.Nil |
100 [THEN zg.ZG1, THEN zg.Reception [of _ A B], |
100 [THEN zg.ZG1, THEN zg.Reception [of _ A B], |
101 THEN zg.ZG2, THEN zg.Reception [of _ B A], |
101 THEN zg.ZG2, THEN zg.Reception [of _ B A], |
102 THEN zg.ZG3, THEN zg.Reception [of _ A TTP], |
102 THEN zg.ZG3, THEN zg.Reception [of _ A TTP], |
103 THEN zg.ZG4]) |
103 THEN zg.ZG4]) |
104 apply (possibility, auto) |
104 apply (basic_possibility, auto) |
105 done |
105 done |
106 |
106 |
107 subsection {*Basic Lemmas*} |
107 subsection {*Basic Lemmas*} |
108 |
108 |
109 lemma Gets_imp_Says: |
109 lemma Gets_imp_Says: |