Changeset 2316 for src/ASM/Policy.ma
- Timestamp:
- Sep 3, 2012, 9:03:24 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2264 r2316 186 186 policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) 187 187 (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). 188 #program #n #Heq cases daemon (* XXX *) 188 #program #n #Heq inversion (jump_expansion_internal program n) #x cases x -x 189 #no_ch #pol cases pol normalize nodelta 190 [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O 191 #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by / 192 | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???); 193 lapply (refl ? (jump_expansion_internal program (S n))) 194 whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn 195 normalize nodelta inversion no_ch #Hno_ch normalize nodelta #Seq >Seq 196 [ #Heq lapply (refl ? (jump_expansion_internal program (S (S n)))) 197 whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq 198 normalize nodelta #Teq >Teq @pe_refl 199 | #Heq lapply (refl ? (jump_expansion_internal program (S (S n)))) 200 whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq 201 normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*) 202 #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol 203 [ normalize nodelta #HSn #Heq #Seq cases Heq 204 | -Spol #Spol normalize nodelta cases Sno_ch normalize nodelta #HSn #Heq #Seq 205 [ @pe_refl 206 | cases daemon 207 ] 208 ] 209 ] 210 ] 189 211 qed. 190 212 … … 445 467 [ lapply (jump_pc_equal program (2*|program|)) 446 468 >Feq >Geq normalize nodelta #H @H @Heq 469 | @Heq 447 470 | cases daemon (* true, but have to add this to properties *) 471 | cases daemon 448 472 | @(proj2 ?? (proj1 ?? HGp)) 449 473 ]
Note: See TracChangeset
for help on using the changeset viewer.