Changeset 3479 for LTS/Language.ma


Ignore:
Timestamp:
Sep 22, 2014, 5:14:56 PM (5 years ago)
Author:
sacerdot
Message:

Repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3478 r3479  
    608608                             | _ ⇒ false
    609609                             ]
    610 | init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false]
    611610].
    612611
     
    17681767    * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
    17691768    cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
    1770     [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) *****
     1769    [ #x #y #_ (*#_ #_ #_ #H*) *****
    17711770    | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
    17721771      normalize * /2/ ] *
     
    18681867        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    18691868      %
    1870       [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
     1869      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
     1870          >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*)
    18711871          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
    18721872          @is_permutation_cons assumption
     
    19131913      ]
    19141914    ]
    1915     #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?);
     1915    #seq1 #opt_l #i' #_ #EQcode_s1' cases daemon (*CSC: ROTTO QUI
     1916    change with (m_bind ?????) in ⊢ (??%? → ?);
    19161917    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
    19171918    * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta
     
    19411942          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    19421943      ]]
    1943     %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
     1944    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct *)
    19441945  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    19451946    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    22772278  inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****]
    22782279  * #gen_labs #i' #EQi' inversion act_lab normalize nodelta
    2279   [ #f #lab | * [| #lbl1 ]| * [| #nf_l] |] #EQ destruct(EQ)
     2280  [ #f #lab | * [| #lbl1 ]| * [| #nf_l]] #EQ destruct(EQ)
    22802281  [1,6: whd in ⊢ (??%% → ?); #EQ destruct *****
    22812282  |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct
     
    23852386    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh'
    23862387    #EQenv_it' ***** #EQtrans
    2387     #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
     2388    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: WAS WORKING
    23882389    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
    23892390    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
     
    24342435        ]
    24352436    | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    2436     ]
     2437    ] *)
    24372438  ]
    24382439| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
     
    25022503    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
    25032504    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans
    2504     #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
     2505    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: was working
    25052506    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
    25062507    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
     
    26302631       ]
    26312632     ]
    2632 ]
    2633 qed.
     2633*)]
     2634qed.
Note: See TracChangeset for help on using the changeset viewer.