1Kind name,action,proc type. 2 3Import "ccs_bisim_context". 4Import "ccs_ctx". 5Import "ccs_bisim_examples_helper". 6 7Theorem bisim_context_reflexive_ : forall P, 8 bisim_up_to bisim_context_t P P. 9coinduction. intros. unfold. 10 intros. 11 witness P1. split. search. 12 witness P1. witness P1. split. 13 unfold. witness P1. witness P1. split. 14 unfold. 15 backchain bisim_reflexive_. 16 backchain bisim_reflexive_. 17 search. 18 backchain CH. 19 intros. 20 witness Q1. split. search. 21 witness Q1. witness Q1. split. 22 unfold. witness Q1. witness Q1. split. 23 unfold. 24 backchain bisim_reflexive_. 25 backchain bisim_reflexive_. 26 search. 27 backchain CH. 28 29Theorem bisim_repl_absorb : forall P, 30 bisim_up_to refl_t (par (repl P) P) (repl P). 31Sound : apply bisim_context_sound. Sound : case Sound. 32intros. backchain Sound. clear Sound. 33coinduction. intros. unfold. 34 intros. case H1. 35 case H2. 36 witness (par (repl P) Q). split. search. 37 witness (par (repl P) P). 38 witness (repl P). split. unfold. 39 witness (par (par (repl P) P) Q). 40 witness (par (repl P) Q). split. unfold. 41 backchain bisim_par_assoc_left. 42 backchain bisim_reflexive_. 43 search. 44 backchain CH. 45 witness (par (repl P) (par Q R)). split. search. 46 witness (par (repl P) P). 47 witness (repl P). split. unfold. 48 witness (par (par (repl P) P) (par Q R)). 49 witness (par (repl P) (par Q R)). split. unfold. 50 backchain bisim_par_assoc_left. 51 backchain bisim_reflexive_. 52 search. 53 backchain CH. 54 witness (par (repl P) Q1). split. search. 55 witness (par (repl P) Q1). 56 witness (par (repl P) Q1). split. unfold. 57 witness (par (repl P) Q1). 58 witness (par (repl P) Q1). split. unfold. 59 backchain bisim_reflexive_. 60 backchain bisim_reflexive_. 61 search. 62 backchain bisim_context_reflexive_. 63 case H2. 64 witness (par (repl P) (par Q Q1)). split. search. 65 witness (par (repl P) (par Q Q1)). 66 witness (par (repl P) (par Q Q1)). split. unfold. 67 witness (par (repl P) (par Q Q1)). 68 witness (par (repl P) (par Q Q1)). split. unfold. 69 backchain bisim_par_assoc. 70 backchain bisim_reflexive_. 71 search. 72 backchain bisim_context_reflexive_. 73 case H2. 74 witness (par (repl P) (par Q1 Q)). split. search. 75 witness (par (repl P) (par Q1 Q)). 76 witness (par (repl P) (par Q1 Q)). split. unfold. 77 witness (par (repl P) (par Q1 Q)). 78 witness (par (repl P) (par Q1 Q)). split. unfold. 79 apply bisim_par_comm with P = Q, Q = Q1. 80 apply bisim_par_subst_2 to H5 with R = (repl P). 81 apply bisim_par_assoc with P = (repl P), Q = Q, R = Q1. 82 backchain bisim_transitive_. 83 backchain bisim_reflexive_. 84 search. 85 backchain bisim_context_reflexive_. 86 intros. case H1. 87 witness (par (par (repl P) Q) P). split. search. 88 witness (par (repl P) P). 89 witness (repl P). split. unfold. 90 witness (par (par (repl P) P) Q). 91 witness (par (repl P) Q). split. unfold. 92 backchain bisim_par_assoc_left. 93 backchain bisim_reflexive_. 94 search. 95 backchain CH. 96 witness (par (par (repl P) (par Q R)) P). split. search. 97 witness (par (repl P) P). 98 witness (repl P). split. unfold. 99 witness (par (par (repl P) P) (par Q R)). 100 witness (par (repl P) (par Q R)). split. unfold. 101 backchain bisim_par_assoc_left. 102 backchain bisim_reflexive_. 103 search. 104 backchain CH. 105 106 107%%% !(a.P + b.Q) ~ (!a.P | !b.Q) 108 109Theorem ex_bang_plus_ctx : forall P, 110 bisim (repl (plus (act (dn a) P) (act (dn b) P))) 111 (par (repl (act (dn a) P)) (repl (act (dn b) P))). 112Sound : apply bisim_context_sound. Sound : case Sound. 113intros. unfold. backchain Sound. clear Sound. 114coinduction. intros. unfold. 115 intros. case H1. 116 case H2. 117 case H3. 118 witness (par (par (repl (act (dn a) P)) P) (repl (act (dn b) P))). split. search. 119 witness (repl (plus (act (dn a) P) (act (dn b) P))). 120 witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold. 121 witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). 122 witness (par (par (repl (act (dn a) P)) (repl (act (dn b) P))) P). split. unfold. 123 backchain bisim_reflexive_. 124 apply bisim_par_comm with P = P, Q = (repl (act (dn b) Q)). 125 apply bisim_par_subst_2 to H4 with R = (repl (act (dn a) Q)). 126 apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = P, R = (repl (act (dn b) Q)). 127 apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = (repl (act (dn b) Q)), R = P. 128 apply bisim_transitive_ to H6 H5. 129 apply bisim_symmetric_ to H7. 130 apply bisim_transitive_ to H8 H9. 131 search. 132 search. 133 backchain CH. 134 case H3. 135 witness (par (repl (act (dn a) P)) (par (repl (act (dn b) P)) P)). split. search. 136 witness (repl (plus (act (dn a) P) (act (dn b) P))). 137 witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold. 138 witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). 139 witness (par (par (repl (act (dn a) P)) (repl (act (dn b) P))) P). split. unfold. 140 backchain bisim_reflexive_. 141 apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = (repl (act (dn b) Q)), R = Q. 142 backchain bisim_symmetric_. 143 search. 144 backchain CH. 145 case H2. 146 case H4. 147 case H4. 148 intros. case H1. 149 case H2. 150 case H3. 151 witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). split. search. 152 witness (repl (plus (act (dn a) P) (act (dn b) P))). 153 witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold. 154 witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). 155 witness (par (par (repl (act (dn a) P)) (repl (act (dn b) P))) P). split. unfold. 156 backchain bisim_reflexive_. 157 apply bisim_par_comm with P = Q, Q = (repl (act (dn b) Q)). 158 apply bisim_par_subst_2 to H4 with R = (repl (act (dn a) Q)). 159 apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = Q, R = (repl (act (dn b) Q)). 160 apply bisim_par_assoc with P = (repl (act (dn a) Q)), Q = (repl (act (dn b) Q)), R = Q. 161 apply bisim_transitive_ to H6 H5. 162 apply bisim_symmetric_ to H7. 163 apply bisim_transitive_ to H8 H9. 164 search. 165 search. 166 backchain CH. 167 case H3. 168 case H2. 169 case H3. 170 witness (par (repl (plus (act (dn a) P) (act (dn b) P))) P). split. search. 171 witness (repl (plus (act (dn a) P) (act (dn b) P))). 172 witness (par (repl (act (dn a) P)) (repl (act (dn b) P))). split. unfold. 173 witness par (repl (plus (act (dn a) P) (act (dn b) P))) Q. 174 witness par (par (repl (act (dn a) P)) (repl (act (dn b) P))) Q. split. unfold. 175 backchain bisim_reflexive_. 176 apply bisim_par_assoc with P = (repl (act (dn a) P)), Q = (repl (act (dn b) P)), R = Q. 177 backchain bisim_symmetric_. 178 search. 179 backchain CH. 180 case H3. 181 case H2. 182 case H4. 183 case H3. 184 case H4. 185 186 187%%% !!a.P ~ !a.P 188 189Theorem ex_bang_bang_ctx : forall P, 190 bisim (repl (repl (act (dn a) P))) 191 (repl (act (dn a) P)). 192Sound : apply bisim_context_sound. Sound : case Sound. intros. 193unfold. backchain Sound. clear Sound. 194coinduction. intros. unfold. 195 intros. case H1. 196 case H2. 197 case H3. 198 witness (par (repl (act (dn a) P)) P). split. search. 199 witness (repl (repl (act (dn a) P))). 200 witness (repl (act (dn a) P)). split. unfold. 201 witness (par (repl (repl (act (dn a) P))) P). 202 witness (par (repl (act (dn a) P)) P). split. unfold. 203 apply bisim_repl_absorb with P = (repl (act (dn a) P)). 204 apply bisim_par_subst_1 to H4 with R = P. 205 apply bisim_par_assoc with P = (repl (repl (act (dn a) P))), Q = (repl (act (dn a) P)), R = P. 206 apply bisim_symmetric_ to H6. 207 apply bisim_transitive_ to H7 H5. 208 search. 209 backchain bisim_reflexive_. 210 search. 211 backchain CH. 212 case H3. 213 case H2. 214 case H4. 215 216 intros. case H1. 217 case H2. 218 witness (par (repl (repl (act (dn a) P))) (par (repl (act (dn a) P)) P)). split. search. 219 witness (repl (repl (act (dn a) P))). 220 witness (repl (act (dn a) P)). split. unfold. 221 witness (par (repl (repl (act (dn a) P))) P). 222 witness (par (repl (act (dn a) P)) P). split. unfold. 223 apply bisim_repl_absorb with P = (repl (act (dn a) P)). 224 apply bisim_par_subst_1 to H3 with R = P. 225 apply bisim_par_assoc with P = (repl (repl (act (dn a) P))), Q = (repl (act (dn a) P)), R = P. 226 apply bisim_symmetric_ to H5. 227 apply bisim_transitive_ to H6 H4. 228 search. 229 backchain bisim_reflexive_. 230 search. 231 backchain CH. 232 case H2. 233