Changeset 3540 for LTS/Lang_meas.ma


Ignore:
Timestamp:
Mar 17, 2015, 7:33:34 PM (5 years ago)
Author:
piccolo
Message:

closed some daemons

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Lang_meas.ma

    r3535 r3540  
    3939    * #labels #code_cleaned #EQclean normalize nodelta
    4040    >EQcode in EQcall_post; inversion(code ? s1')
    41         [2,3,4,5,6,7: cases daemon (*ASSURDI*)
     41        [2,3,4,5,6,7:
     42          [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     43            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
     44          #_ whd in ⊢ (??%% → ?);
     45          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     46          | cases(call_post_clean ?????); normalize nodelta
     47            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     48               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     49                 [| #z cases(?∧?) normalize nodelta
     50                 ]
     51               ]
     52            ]
     53          | cases(call_post_clean ?????) normalize nodelta
     54            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     55               [| #y cases(?∧?) normalize nodelta
     56               ]
     57            ]
     58          | cases(call_post_clean ?????) normalize nodelta
     59             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     60                [ cases (?==?) normalize nodelta ]
     61             ]]
     62          | cases(call_post_clean ?????) normalize nodelta
     63             [| #x cases(? ∧ ?) normalize nodelta ]
     64          ]
     65          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    4266        | #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct cases lab' normalize nodelta
    4367          [ #f #c whd in ⊢ (??%% → ?); #EQ destruct %{(refl …)} cases HHcont
     
    5175  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
    5276  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode_s1 inversion(code ? s1')
    53   [1,2,4,5,6,7: cases daemon (* ASSURDI*)
     77  [1,2,4,5,6,7:
     78    [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     79            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
     80          #_ whd in ⊢ (??%% → ?);
     81          [ |
     82          | cases(call_post_clean ?????); normalize nodelta
     83            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     84               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     85                 [| #z cases(?∧?) normalize nodelta
     86                 ]
     87               ]
     88            ]
     89          | cases(call_post_clean ?????) normalize nodelta
     90            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     91               [| #y cases(?∧?) normalize nodelta
     92               ]
     93            ]
     94          | cases(call_post_clean ?????) normalize nodelta
     95             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     96                [ cases (?==?) normalize nodelta ]
     97             ]]
     98          | cases(call_post_clean ?????) normalize nodelta
     99             [| #x cases(? ∧ ?) normalize nodelta ]
     100          ]
     101          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    54102  | #i' * [|#lb] #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    55103    [1,3: #EQ destruct] #x whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
     
    57105    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ4 destruct
    58106 ]
    59 | cases daemon
     107| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ destruct #EQ destruct
     108  #Hio1 #Hio2 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
     109  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
     110  [1,2,3,5,6,7:
     111    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
     112       | #lin #io #lout #instr #_ ]
     113          #_ whd in ⊢ (??%% → ?);
     114          [ |
     115          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     116          | cases(call_post_clean ?????) normalize nodelta
     117            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     118               [| #y cases(?∧?) normalize nodelta
     119               ]
     120            ]
     121          | cases(call_post_clean ?????) normalize nodelta
     122             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     123                [ cases (?==?) normalize nodelta ]
     124             ]]
     125          | cases(call_post_clean ?????) normalize nodelta
     126             [| #x cases(? ∧ ?) normalize nodelta ]
     127          ]
     128          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     129  ]
     130  cases daemon (*TODO*)
    60131| cases daemon
    61132| cases daemon
Note: See TracChangeset for help on using the changeset viewer.