Changeset 2944


Ignore:
Timestamp:
Mar 23, 2013, 2:31:23 AM (4 years ago)
Author:
sacerdot
Message:

Some progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2942 r2944  
    649649    #EQst1st2 #_ #_
    650650    (* CSC: END *)
    651     lapply (sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
    652     XXXX
    653     <EQst1st2
    654    
    655     lapply Heval_seq_no_pc; whd in match eval_seq_no_pc; normalize nodelta
    656    
    657      whd in Heval_seq_no_pc:(??%%); whd in match (st_no_pc ??);
    658 
    659 
    660        
    661        
    662        
    663         <(injective_OK ??? EQst1_no_pc)
    664         change with (set_regs ???) in match (st_no_pc ??);
     651    letin before ≝ (livebefore ???)
     652    whd in match succ_pc; normalize nodelta >point_of_pc_of_point
     653    whd in match (point_of_succ ???);
     654    cut (before nxt = before (point_of_pc ERTLptr_semantics (pc … st1)))
     655    [ YYY whd in ⊢ (??%%); whd in EQstmt; whd in EQstmt:(??%?); >EQstmt
     656      (* Ha funzionato solo a dx, non a sinistra...*)
     657      normalize nodelta whd in match statement_semantics; normalize nodelta
     658      >Heliminable
     659     cases daemon (*CSC: Genuine proof obligation! *)
     660    | #Hext ]
     661    >(to_be_cleared_fb_respects_equal_valuations … Hext)
     662    >(sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
     663    >EQst1st2
     664    >(to_be_cleared_sb_respects_equal_valuations … Hext) %
     665|
     666|
    665667 
     668  XXXX
    666669 
    667670  *
Note: See TracChangeset for help on using the changeset viewer.