Changeset 1713 for src/Clight/CexecSound.ma
 Timestamp:
 Feb 21, 2012, 11:58:12 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecSound.ma
r1672 r1713 511 511 ] 512 512  #v #k' #m' whd in ⊢ (?????%); cases k'; //; 513 #r #f #e #k whd in ⊢ (?????%); cases r; 514 [ whd; @step_returnstate_0 515  #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty 516 @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //; 517 ] 513 [ whd in ⊢ (?????%); cases v // * // 514  #r #f #e #k whd in ⊢ (?????%); cases r // 515 * * #b #ofs #ty 516 @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); // 517 ] 518  // 518 519 ] 519 520 qed. … … 536 537 [ whd; % 537 538  @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s'; 538 [ #f #s #k #e #m  #fd #args #k #m  #r #k #m ] normalize 539 (* whd in ⊢ (? → ?????(??????%?)); *) 540 cases m; #mc #mn #mp #Hstep normalize 541 (* whd in ⊢ (?????(??????%?));*) 539 [ #f #s #k #e #m  #fd #args #k #m  #r #k #m  #r ] normalize 540 [ 1,2,3: cases m; #mc #mn #mp ] #Hstep normalize 542 541 @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps 543 whd; @(star_step ????????? Hsteps) [ 2,5,8 : @Hstep  3,6,9: // ]542 whd; @(star_step ????????? Hsteps) [ 2,5,8,11: @Hstep  3,6,9,12: // ] 544 543 ] 545 544 qed. 546 545 547 546 lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r. 548 * [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct % 549  *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct 550 ] 551  *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct 552 ] 553  *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct 547 * [ 4: #r #r' normalize #E destruct % 548  *: normalize #x1 #x2 #x3 #x4 #x5 try #x6 try #x7 destruct 554 549 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.