Changeset 3406
- Timestamp:
- Dec 23, 2013, 10:22:24 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3405 r3406 883 883 qed. 884 884 885 885 lemma eq_a_non_functional_label : 886 ∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2. 887 #c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ 888 #EQ destruct >(\b (refl …)) @I 889 qed. 886 890 887 891 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. … … 999 1003 whd in match (get_element ????); >(\b (refl …)) normalize nodelta 1000 1004 >(\b (refl …)) % 1001 |*: cases daemon (*TODO*) 1002 ] 1005 | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); 1006 #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on 1007 whd in ⊢ (??%?); >IH2 1008 [ normalize nodelta >IH1 1009 [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ] 1010 whd in match (get_element ????); 1011 inversion(a_non_functional_label ltrue == a_non_functional_label lfalse) 1012 #Hltrue normalize nodelta 1013 [ cases no_dup whd in match (memb ???); 1014 cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse)) 1015 #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ] 1016 whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) 1017 <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ] 1018 whd in match (get_element ????); >(\b (refl …)) normalize nodelta 1019 >(\b (refl …)) % 1020 | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?); 1021 @(same_to_keep_on_append … keep_on) // [ #x * | #x /2 by lab_to_keep_in_domain/ ] 1022 | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map) 1023 /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse 1024 normalize nodelta 1025 [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse % 1026 | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_ 1027 @orb_Prop_l >Hltrue % 1028 ] 1029 | % 1030 | cases no_dup #_ * #_ /2/ 1031 | 1032 ] 1033 | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on; 1034 <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?); 1035 >associative_append in ⊢ (??%? → ?); #keep_on @(same_to_keep_on_append … keep_on) 1003 1036 qed. 1004 1037
Note: See TracChangeset
for help on using the changeset viewer.