Changeset 3404 for LTS/Language.ma


Ignore:
Timestamp:
Dec 19, 2013, 7:43:28 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3403 r3404  
    995995      whd in match (memb ???); >(\b (refl …)) % ]
    996996      whd in match (get_element ????); @eq_costlabel_elim normalize nodelta
    997       [ #ABS cases daemon (*CSC: FALSO!! *) ] #_ whd in match (get_element ????);
    998       >(\b (refl …)) normalize nodelta >(\b (refl …)) %
     997      [ #ABS @⊥ cases no_dup >ABS * #H #_ @H @orb_Prop_l 
     998      >(\b (refl ? (a_non_functional_label ltrue))) % ] #_
     999      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
     1000      >(\b (refl …)) %
    9991001|*: cases daemon (*TODO*)
    10001002]
     
    10711073f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧
    10721074same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info).
    1073 #p * #env #main @pair_elim * #t_prog #m #keep whd in match trans_prog;
    1074 normalize nodelta @pair_elim generalize in match O; xxxx (*probably needs invariant *) elim env
    1075 [ * #env' #fresh #x #_ #_ #_ #f #env_it normalize in ⊢ (% → ?);  #ABS destruct]
    1076 * #hd_sig #hd_lab #hd_code #tail #IH * #env' #fresh * #m' #keep'
     1075#p * #env #main @pair_elim * whd in match trans_prog; normalize nodelta
     1076@pair_elim generalize in match O; (*probably needs invariant *) elim env
     1077[ #fresh1 * #env' #fresh #x #_ #t_prog #m #keep #_ #_ #f #env_it normalize in ⊢ (% → ?);  #ABS destruct]
     1078* #hd_sig #hd_lab #hd_code #tail #IH #fresh1 * #env' #fresh * #m' #keep'
    10771079normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail
    1078 * #m_tail #keep_tail #EQtail normalize nodelta #EQ1 #EQ2 destruct(EQ1 EQ2)
     1080* #m_tail #keep_tail #EQtail normalize nodelta #EQ1 destruct(EQ1) #t_prog
     1081#m #keep #EQ2 destruct(EQ2)
    10791082whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H)
    10801083change with (no_duplicates_labels p p (mk_Program p p tail main)) in match
     
    10931096  ]
    10941097| #Hf #Henv_it cases(IH … no_dup_tail … Henv_it)
    1095   [4: >EQtail in ⊢ (??%?);
     1098  [5: >EQtail in ⊢ (??%?); %
     1099  |9: normalize nodelta %
     1100  |*:
     1101  ]
     1102  #new_env_it * #new_fresh * #EQlook_new_env_it ***** #EQt_code #EQ_get_el
     1103  #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh}
     1104  %
     1105     [ whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %]
     1106        #_ normalize nodelta assumption ]
     1107   % [2: #x #Hx <same_to_keep
     1108 
    10961109   
    10971110   
Note: See TracChangeset for help on using the changeset viewer.