Changeset 3406

Timestamp:

Dec 23, 2013, 10:22:24 AM (6 years ago)

Author:

piccolo

Message:

 

File:

• LTS/Language.ma (modified) (2 diffs)

LTS/Language.ma

@@ -883 +883 @@
 qed.
 
- 
+lemma eq_a_non_functional_label : 
+∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2.
+#c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
+#EQ destruct >(\b (refl …)) @I
+qed.
   
 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
@@ -999 +1003 @@
       whd in match (get_element ????); >(\b (refl …)) normalize nodelta
       >(\b (refl …)) % 
-|*: cases daemon (*TODO*)
-]
+| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
+  #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on 
+  whd in ⊢ (??%?); >IH2 
+  [ normalize nodelta >IH1
+    [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ]
+      whd in match (get_element ????);
+      inversion(a_non_functional_label ltrue == a_non_functional_label lfalse) 
+      #Hltrue normalize nodelta
+      [ cases no_dup whd in match (memb ???); 
+        cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse))
+        #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ]
+      whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …))
+      <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ] 
+      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
+      >(\b (refl …)) %
+    | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?);
+      @(same_to_keep_on_append … keep_on) // [ #x * | #x /2 by lab_to_keep_in_domain/ ]
+    | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map)
+      /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse
+      normalize nodelta
+      [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse %
+      | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_
+        @orb_Prop_l >Hltrue %
+      ]
+    | %
+    | cases no_dup #_ * #_ /2/
+    |
+    ]
+  | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on; 
+    <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?); 
+    >associative_append in ⊢ (??%? → ?); #keep_on  @(same_to_keep_on_append … keep_on)
 qed.