Changeset 2417 for src/joint

Timestamp:

Oct 25, 2012, 4:36:07 PM (7 years ago)

Author:

boender

Message:

• reverted changes to StructuredTraces? (shouldn't have been committed yet)
• updated _jaap files to remove function identifier from cl_call and add an as_call predicate

Location:

src/joint

Files:

• Joint_jaap.ma (modified) (1 diff)
• stacksize.ma (modified) (3 diffs)

src/joint/Joint_jaap.ma

@@ -175 +175 @@
   [ step_seq s ⇒
     match s with
-    [ CALL_ID l _ _ ⇒    cl_call l
-    | extension_call _ ⇒ cl_call ? (* pointer stuff not yet implemented, it seems *)
+    [ CALL_ID _ _ _ ⇒    cl_call
+    | extension_call _ ⇒ cl_call 
     | _ ⇒ cl_other
     ]
   | COND _ _ ⇒ cl_jump
   ].
- cases daemon
-qed.
 
 record stmt_params : Type[1] ≝

src/joint/stacksize.ma

@@ -47 +47 @@
   [ tal_base_not_return s1 s2 ex cl co ⇒ res
   | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
-  | tal_base_call s1p s1s s2 ex f cl ar tlr co ⇒
+  | tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒
     extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res)
-  | tal_step_call end s1p s1s s1a s2 ex f cl ar tlr co tal ⇒ 
+  | tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒ 
     let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in
     extract_list_from_tal … lg top_f … tal res'
@@ -81 +81 @@
   ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
   extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
+  match t1 with
+  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
+  | tal_base_return st1 st1' ex cl ⇒ ?
+  | tal_base_call st1p st1s st1' ex cl f ca ar tlr1 co ⇒ ?
+  | tal_step_call end st1p st1s st1 st1' ex cl f ca ar tlr1 co tal1 ⇒ ?
+  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
+  ].
+[ cases t2
+  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
+  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
+  ]
+| cases t2
+  [ #st2 #st2' #tll2 normalize #abs cases abs
+  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
+    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
+    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
+  ]
+| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
+  @(tal_rel_extract_equal … H2)
+| cases t2 
+  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
+  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
+  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
+    #taa * #H * #G * #K inversion taa in ⊢ ?;
+    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize #abs destruct (abs)
+    ]
+  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize *
+    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
+    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize #abs destruct (abs)
+    ]
+  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
+    * #H * #G * #K inversion taa in ⊢ ?;
+    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 
+      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
+    ]
+  ]
+| cases t2
+  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
+  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 
+  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #abs destruct (abs) 
+  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
+    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
+    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize #abs destruct (abs)
+    ]
+  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
+    * #taa * #H * #G inversion taa in ⊢ ?;
+    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)  
+    ]
+  ]
+| cases t2
+  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
+    * #st2mid' * #H * * [2: #st2mid'' *] #J * #f' * #G * #K * #tlr2 * #L * #H1
+    [ * * #H3 #H2 #H4 | #H2 ]
+    inversion taa in ⊢ ?;
+    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
+    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize in H3; destruct (H3)
+    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
+    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize in H1; destruct (H1)
+    ]
+  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
+  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #_ * #st2mid *
+    #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f'' * #G * #K * #tlr2' * #L
+    inversion taa in ⊢ ?;
+    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #tal2 * * #H1 destruct (H1)
+    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * #tal2 * * #H1 destruct (H1)
+    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
+      >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
+    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * #abs destruct (abs)
+    ]
+  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
+    normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f
+    * #G * #K * #tlr2' * #L
+    inversion taa in ⊢ ?;
+    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3 #res
+      cases daemon
+    | #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * #tal2' * * #H1 destruct (H1)
+    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * #abs destruct (abs)
+    ]
+  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
+    #taa * #st2mid' * #H * * [2: #stmid'' * ] #J * #f * #G * #K * #tlr2 * #L
+    inversion taa in ⊢ ?;
+    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 destruct (H1)
+    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * #tal2' * * #H1 #H2 #H3 #res cases daemon
+    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *) 
+    ]
+  ]
+| cases t2
+  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun *
+    #st2_after_fun * * [#H | #st2mid'] * #J * #f' * #G * #K * #tlr2 * #L [2: * #tl2]
+    inversion taa in ⊢ ?;
+    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
+    | #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize * * #H1 destruct (H1)
+    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
+    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize * * #abs destruct (abs)
+    ]
+  | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2mid' * #H *
+    [ * #abs destruct (abs) | * #st2mid'' * #J * #f' * #G * #K * #tlr2 * #L * #tl2
+      inversion taa in ⊢ ?;
+      [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
+      | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+        normalize * * #abs destruct (abs)
+      ]
+    ]
+  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #st2mid * #taa
+    * #st2mid' * #H * * [ #_ | #st2mid'' ] * #J * #f'' * #G * #K * #tlr2' * #L [2: * #tl2]
+    inversion taa in ⊢ ?;
+    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * * #abs destruct (abs)
+    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 cases daemon 
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * * #abs destruct (abs)
+    ]
+  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
+    normalize * #st2mid * #taa * #st2mid' * #ex'' * * [ #_ | #st2mid''] * #J *
+    #f'' * #G * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
+    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
+      cases daemon (* injectivity needed again *)
+    | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * * #abs destruct (abs)
+    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) cases daemon
+      (* huh? *)
+    | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * * #abs destruct (abs) cases daemon (* huh2? *)
+    ]
+  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
+    #st2mid' * #H * * [ #He | #st2mid'' ] * #J * #f' * #G * #K * #tlr2' * #L
+    [2: * #tl2] inversion taa in ⊢ ?;
+    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)
+    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
+    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
+      destruct normalize * * #H1 #H2 #H3 #res cases daemon 
+    ]
+  ]
+| cases t2
+  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
+    @(tal_rel_extract_equal p g lg top_f … Hsim) 
+  | #ss #fs #ex' #cl' normalize #Hsim #res 
+    @(tal_rel_extract_equal p g lg top_f … Hsim) 
+  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize #Hsim #res
+    @(tal_rel_extract_equal p g lg top_f … Hsim)
+  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
+    normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
+  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
+    @(tal_rel_extract_equal p g lg top_f … Hsim)
+  ]
+]
+qed.
+
+(* let rec tlr_rel_max_equal (p: params) (g: list ident)
+  (lg: ident → joint_internal_function p g) (top_f: ident)
+  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
+  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
+  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
+  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
+  match t1 with
+  [ tlr_base st1 st1' tll1 ⇒ ?
+  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
+  ]
+and tll_rel_extract_equal (p: params) (g: list ident)
+  (lg: ident → joint_internal_function p g) (top_f: ident)
+  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
+  t1 ≈ t2 →
+  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
+  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
+  match t1 with
+  [ tll_base ends st1 st1' tal1 co ⇒ ?
+  ]
+and tal_rel_extract_equal (p: params) (g: list ident)
+  (lg: ident → joint_internal_function p g) (top_f: ident)
+  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
+  t1 ≈ t2 →
+  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
+  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
   match t1 with
   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
@@ -88 +285 @@
   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
   ].
-[ cases t2
-  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
-  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
-  ]
-| cases t2
-  [ #st2 #st2' #tll2 normalize #abs cases abs
-  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
-    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
-    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
-  ]
-| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
-  @(tal_rel_extract_equal … H2)
-| cases t2 
-  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
-  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
-  | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
-    #taa * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 normalize *
-    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
-    * #H * #G * #K inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 
-      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
-  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 
-  | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 
-  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
-    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
-    * #taa * #H * #G inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)  
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
-    * #st2mid' * #H * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?;
-    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
-    | #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize in H1; destruct (H1)
-    ]
-  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
-  | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid *
-    #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?;
-    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
-      >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
-    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
-    normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L
-    inversion taa in ⊢ ?;
-    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
-    #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?;
-    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *) 
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
-    * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize * * #abs destruct (abs)
-    ]
-  | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
-    * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
-      normalize * * #abs destruct (abs)
-    ]
-  | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa
-    * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2
-    inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
-    normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' *
-    #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
-      >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #abs destruct (abs)
-    ]
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
-    #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2 
-    inversion taa in ⊢ ?;
-    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
-    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
-      destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *) 
-    ]
-  ]
-| cases t2
-  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
-    @(tal_rel_extract_equal p g lg top_f … Hsim) 
-  | #ss #fs #ex' #cl' normalize #Hsim #res 
-    @(tal_rel_extract_equal p g lg top_f … Hsim) 
-  | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res
-    @(tal_rel_extract_equal p g lg top_f … Hsim)
-  | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
-    normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
-  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
-    @(tal_rel_extract_equal p g lg top_f … Hsim)
-  ]
-]
-qed.
-
-let rec tlr_rel_max_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
-  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
-  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
-  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
-  match t1 with
-  [ tlr_base st1 st1' tll1 ⇒ ?
-  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
-  ]
-and tll_rel_extract_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
-  t1 ≈ t2 →
-  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
-  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
-  match t1 with
-  [ tll_base ends st1 st1' tal1 co ⇒ ?
-  ]
-and tal_rel_extract_equal (p: params) (g: list ident)
-  (lg: ident → joint_internal_function p g) (top_f: ident)
-  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
-  t1 ≈ t2 →
-  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
-  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
-  match t1 with
-  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
-  | tal_base_return st1 st1' ex cl ⇒ ?
-  | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
-  | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
-  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
-  ].
  cases daemon (* next proof *)
-qed.
+qed. *)