Changeset 2239 for src/ASM/PolicyStep.ma
 Timestamp:
 Jul 24, 2012, 11:09:29 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2238 r2239 232 232 qed. 233 233 234 lemma jump_expansion_step4: 235 ∀labels : label_map. 236 ∀old_sigma : ppc_pc_map. 237 ∀prefix : list (option Identifier×pseudo_instruction). 238 ∀inc_added : ℕ. 239 ∀inc_pc_sigma : ppc_pc_map. 240 ∀label : option Identifier. 241 ∀instr : pseudo_instruction. 242 ∀inc_pc : ℕ. 243 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. 244 ∀old_length : jump_length. 245 ∀Hpolicy1 : sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉. 246 ∀Hpolicy2: inc_pc 247 =\fst (lookup … (bitvector_of_nat … (prefix)) inc_sigma 248 〈O,short_jump〉). 249 ∀Hpolicy3: out_of_program_none prefix 〈inc_pc,inc_sigma〉. 250 ∀policy : ppc_pc_map. 251 ∀new_length : jump_length. 252 ∀isize : ℕ. 253 ∀Heq1 : 254 match 255 match instr 256 in pseudo_instruction 257 return λ_:pseudo_instruction.(option jump_length) 258 with 259 [Instruction (i:(preinstruction Identifier))⇒ 260 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 261 (prefix) i 262 Comment (_:String)⇒None jump_length 263 Cost (_:costlabel)⇒None jump_length 264 Jmp (j:Identifier)⇒ 265 Some jump_length 266 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 267 Call (c:Identifier)⇒ 268 Some jump_length 269 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 270 Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length] 271 in option 272 return λ_:(option jump_length).(jump_length×ℕ) 273 with 274 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 275 Some (pl:jump_length)⇒ 276 〈max_length old_length pl, 277 instruction_size_jmplen (max_length old_length pl) instr〉] 278 =〈new_length,isize〉. 279 ∀prefix_ok1 : S (prefix)< 2 \sup 16. 280 ∀prefix_ok : prefix< 2 \sup 16. 281 ∀Heq2b : 282 〈inc_pc+isize, 283 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 284 〈inc_pc+isize, 285 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 286 (\snd old_sigma) 〈O,short_jump〉)〉 287 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 288 〈inc_pc,new_length〉 inc_sigma)〉 289 =policy. 290 sigma_compact_unsafe (prefix@[〈label,instr〉]) labels policy. 291 #labels #old_sigma #prefix #inc_added #inc_pc_sigma #label #instr #inc_pc #inc_sigma 292 #old_length #Hpolicy1 #Hpolicy2 #Hpolicy3 #policy #new_length #isize 293 #Heq1 #prefix_ok1 #prefix_ok #Heq2b 294 #i >append_length <commutative_plus #Hi normalize in Hi; 295 <Heq2b 296 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 297 [ >lookup_opt_insert_miss 298 [ >lookup_opt_insert_miss 299 [ >lookup_opt_insert_miss 300 [ cases (le_to_or_lt_eq … Hi) Hi #Hi 301 [ >lookup_opt_insert_miss 302 [ (* USE[pass]: sigma_compact_unsafe *) 303 lapply (Hpolicy1 i ?) 304 [ @le_S_to_le @Hi ] 305 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 306 [ normalize nodelta #X @X 307  #x cases x x #x1 #x2 308 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) 309 normalize nodelta 310 [ #X @X 311  #y cases y y #y1 #y2 normalize nodelta >nth_append_first 312 [ #X @X 313  @le_S_to_le @Hi 314 ] 315 ] 316 ] 317  @bitvector_of_nat_abs 318 [3: @lt_to_not_eq @Hi ] 319 ] 320  >Hi >lookup_opt_insert_hit normalize nodelta 321 (* USE[pass]: sigma_compact_unsafe *) 322 lapply (Hpolicy1 i ?) 323 [ <Hi @le_n 324  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 325 [ normalize nodelta #X @X 326  #x cases x x #x1 #x2 327 (* USE: inc_pc = fst inc_sigma *) 328 lapply Hpolicy2 329 <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 330 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); 331 [ normalize nodelta #_ #_ #H cases H 332  #y cases y y #y1 #y2 #Heq >nth_append_first 333 [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) 334 #Heq2 <Heq2 #X @X 335  <Hi @le_n]]]]]]]] 336 [3,4,5: @bitvector_of_nat_abs] 337 [ @(transitive_lt ??? (le_S_S … Hi)) 338 3: @lt_to_not_eq @le_S_S @Hi 339 4,7,10: @(transitive_lt ??? Hi) assumption 340 5,11: @le_S_to_le 341 6: @lt_to_not_eq @Hi 342 9: @lt_to_not_eq @le_S @Hi 343 ] 344 assumption 345  >Hi >lookup_opt_insert_miss 346 [2: @bitvector_of_nat_abs try assumption @lt_to_not_eq % ] 347 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 348 (* USE: out_of_program_none ← *) 349 lapply (Hpolicy3 i ?) 350 [ >Hi assumption 351  >Hi 352 (* USE: inc_pc = fst policy *) 353 lapply Hpolicy2 354 inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma) 355 [ #Heq #_ #H @⊥ @(absurd (prefix > prefix)) 356 [ cases H #_ #X @X % 357  @le_to_not_lt @le_n] 358  * #x1 #x2 #Heq #Hip #_ >nth_append_second 359 [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta 360 >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) 361 cases instr in Heq1; normalize nodelta 362 [1: #pi cases (jump_expansion_step_instruction ??????) normalize nodelta] 363 try (#x #y #Heq1) try (#x #Heq1) try #Heq1 364 @eq_f <(proj2 ?? (pair_destruct ?????? Heq1)) 365 try % <(proj1 ?? (pair_destruct ?????? Heq1)) %]]] 366 qed. 367 368 lemma jump_expansion_step5: 369 ∀labels : label_map. 370 ∀old_sigma : ppc_pc_map. 371 ∀prefix : list (option Identifier×pseudo_instruction). 372 ∀inc_added : ℕ. 373 ∀inc_pc_sigma : ppc_pc_map. 374 ∀label : option Identifier. 375 ∀instr : pseudo_instruction. 376 ∀inc_pc : ℕ. 377 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. 378 ∀old_pc : ℕ. 379 ∀old_length : jump_length. 380 ∀Holdeq : 381 lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) (\snd old_sigma) 382 〈O,short_jump〉 383 =〈old_pc,old_length〉. 384 ∀Hpolicy1 : sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O. 385 ∀Hpolicy2: inc_pc 386 =\fst (lookup … (bitvector_of_nat … (prefix)) inc_sigma 〈O,short_jump〉). 387 ∀added : ℕ. 388 ∀policy : ppc_pc_map. 389 ∀new_length : jump_length. 390 ∀isize : ℕ. 391 let add_instr ≝ match instr with 392 [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 393  Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 394  Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (prefix) i 395  _ ⇒ None ? 396 ] in 397 ∀Heq1 : 398 match add_instr with 399 [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉 400 Some (pl:jump_length)⇒ 401 〈max_length old_length pl, 402 instruction_size_jmplen (max_length old_length pl) instr〉] 403 =〈new_length,isize〉. 404 ∀prefix_ok1 : S (prefix)< 2 \sup 16. 405 ∀prefix_ok : prefix< 2 \sup 16. 406 ∀Heq2a : 407 match add_instr with 408 [None⇒inc_added 409 Some (x0:jump_length)⇒ 410 inc_added+(isizeinstruction_size_jmplen old_length instr)] 411 =added. 412 ∀Heq2b : 413 〈inc_pc+isize, 414 insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 415 〈inc_pc+isize, 416 \snd (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (prefix))) 417 (\snd old_sigma) 〈O,short_jump〉)〉 418 (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 419 〈inc_pc,new_length〉 inc_sigma)〉 420 =policy. 421 sigma_jump_equal (prefix@[〈label,instr〉]) old_sigma policy→added=O. 422 #labels #old_sigma #prefix #inc_added #inc_pc #label #instr #inc_pc #inc_sigma 423 #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added #policy #new_length #isize 424 #Heq1 #prefix_ok1 #prefix_ok #Heq2a #Heq2b 425 <Heq2b #Heq <Heq2a 426 (* USE[pass]: policy_jump_equal → added = 0 *) 427 >Hpolicy1 428 [ cases instr in Heq1 Heq; 429 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % 430 1: #pi normalize nodelta whd in match jump_expansion_step_instruction; 431 normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]] 432 #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 433 #Heq (*CSC: make a lemma here!*) lapply Holdeq Holdeq 434 (* USE: inc_pc = fst inc_sigma *) 435 >Hpolicy2 436 lapply (Heq (prefix) ?) 437 [1,3,5: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 438 Heq >lookup_insert_miss 439 [1,3,5: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 440 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 441 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n % 442 *: @bitvector_of_nat_abs try assumption @lt_to_not_eq %] 443  #i #Hi lapply (Heq i ?) 444 [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi 445  >lookup_insert_miss 446 [ >lookup_insert_miss 447 [ #X @X 448  @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption 449 @lt_to_not_eq @Hi] 450  @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption 451 @lt_to_not_eq @le_S @Hi ]]] 452 qed. 453 234 454 (* One step in the search for a jump expansion fixpoint. *) 235 455 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. … … 400 620 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 401 621 cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H 402  (* sigma_compact_unsafe *) cases daemon (* 403 #i >append_length <commutative_plus #Hi normalize in Hi; 404 <(proj2 ?? (pair_destruct ?????? Heq2)) 405 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 406 [ >lookup_opt_insert_miss 407 [ >lookup_opt_insert_miss 408 [ >lookup_opt_insert_miss 409 [ cases (le_to_or_lt_eq … Hi) Hi #Hi 410 [ >lookup_opt_insert_miss 411 [ (* USE[pass]: sigma_compact_unsafe *) 412 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 413 [ @le_S_to_le @Hi ] 414 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 415 [ normalize nodelta #X @X 416  #x cases x x #x1 #x2 417 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) 418 normalize nodelta 419 [ #X @X 420  #y cases y y #y1 #y2 normalize nodelta >nth_append_first 421 [ #X @X 422  @le_S_to_le @Hi 423 ] 424 ] 425 ] 426  @bitvector_of_nat_abs 427 [3: @lt_to_not_eq @Hi ] 428 ] 429  >Hi >lookup_opt_insert_hit normalize nodelta 430 (* USE[pass]: sigma_compact_unsafe *) 431 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 432 [ <Hi @le_n 433  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 434 [ normalize nodelta #X @X 435  #x cases x x #x1 #x2 436 (* USE: inc_pc = fst inc_sigma *) 437 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 438 <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 439 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); 440 [ normalize nodelta #_ #_ #H cases H 441  #y cases y y #y1 #y2 #Heq >nth_append_first 442 [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) 443 #Heq2 <Heq2 #X @X 444  <Hi @le_n 445 ] 446 ] 447 ] 448 ] 449 ] 450 ] 451 ] 452 ] 453 [3,4,5: @bitvector_of_nat_abs] 454 [ @(transitive_lt ??? (le_S_S … Hi)) 455 3: @lt_to_not_eq @le_S_S @Hi 456 4,7,10: @(transitive_lt ??? Hi) @le_S_to_le 457 5,11: @le_S_to_le 458 6: @lt_to_not_eq @Hi 459 9: @lt_to_not_eq @le_S @Hi 460 ] 461 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 462 <plus_n_Sm @le_S_S @le_plus_n_r 463  >Hi >lookup_opt_insert_miss 464 [2: @bitvector_of_nat_abs 465 [ @le_S_to_le ] 466 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 467 <plus_n_Sm @le_S_S @le_plus_n_r 468  @lt_to_not_eq @le_n 469 ] 470 ] 471 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 472 (* USE: out_of_program_none ← *) 473 lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?)) 474 [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r 475  >Hi 476 (* USE: inc_pc = fst policy *) 477 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 478 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma)) 479 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma) in ⊢ (???% → %); 480 [ #Heq #_ #H @⊥ @(absurd (prefix > prefix)) 481 [ @H % 482  @le_to_not_lt @le_n 483 ] 484  #x cases x x #x1 #x2 #Heq #Hip #_ >nth_append_second 485 [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta 486 >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) 487 cases instr in Heq1; 488 [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 489 <(proj1 ?? (pair_destruct ?????? Heq1)) % 490 4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 491 <(proj1 ?? (pair_destruct ?????? Heq1)) % 492 1: #pi cases pi normalize nodelta 493 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 494 [1,2,3,6,7,24,25: #x #y 495 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 496 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 497 <(proj1 ?? (pair_destruct ?????? Heq1)) % 498 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1 499 <(proj2 ?? (pair_destruct ?????? Heq1)) 500 <(proj1 ?? (pair_destruct ?????? Heq1)) % 501 ] 502 ] 503 ] 504 ] 505 ] 506 ] *) 507  (* policy_jump_equal → added = 0 *) cases daemon (* 508 <(proj2 ?? (pair_destruct ?????? Heq2)) 509 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) 510 (* USE[pass]: policy_jump_equal → added = 0 *) 511 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?) 512 [ cases instr in Heq1 Heq; 513 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % 514 4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 515 #Heq lapply Holdeq Holdeq 516 (* USE: inc_pc = fst inc_sigma *) 517 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 518 lapply (Heq (prefix) ?) 519 [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 520 Heq >lookup_insert_miss 521 [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 522 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 523 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n % 524 2,4: @bitvector_of_nat_abs 525 [1,4: @le_S_to_le] 526 [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 527 <plus_n_Sm @le_S_S @le_plus_n_r 528 4,6: @lt_to_not_eq @le_n 529 ] 530 ] 531 1: #pi cases pi normalize nodelta 532 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 533 [1,2,3,6,7,24,25: #x #y 534 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl 535 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1 536 <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq Holdeq 537 (* USE: inc_pc = fst inc_sigma *) 538 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 539 lapply (Heq (prefix) ?) 540 [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 541 Heq >lookup_insert_miss 542 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit in ⊢ (???(???%) → ?); <(proj1 ?? (pair_destruct ?????? Heq1)) 543 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 544 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by / 545 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 546 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n 547 1,4,7,10,13,16,19,22,25: @le_S_to_le 548 ] 549 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S 550 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 551 ] 552 ] 553 ] 554  #i #Hi lapply (Heq i ?) 555 [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi 556  >lookup_insert_miss 557 [ >lookup_insert_miss 558 [ / by / 559  @bitvector_of_nat_abs 560 [ @(transitive_lt ??? Hi) ] 561 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 562 @le_plus_n_r 563  @lt_to_not_eq @Hi 564 ] 565 ] 566  @bitvector_of_nat_abs 567 [ @(transitive_lt ??? Hi) @le_S_to_le ] 568 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 569 <plus_n_Sm @le_S_S @le_plus_n_r 570  @lt_to_not_eq @le_S @Hi 571 ] 572 ] 573 ] 574 ] 575 ] *) 622  (* sigma_compact_unsafe *) 623 @(jump_expansion_step4 … Heq1 … Heq2b) try assumption 624 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 625 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) 626 @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 627  (* policy_jump_equal → added = 0 *) 628 @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption 629 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) 630 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 576 631  (* added = 0 → policy_pc_equal *) cases daemon 577 632 (* USE[pass]: added = 0 → policy_pc_equal *)
Note: See TracChangeset
for help on using the changeset viewer.