[2398] | 1 | include "basics/lists/list.ma". |
---|
| 2 | include "joint/semantics.ma". |
---|
| 3 | include "common/Executions.ma". |
---|
[2426] | 4 | include "common/StructuredTraces.ma". |
---|
[2398] | 5 | |
---|
| 6 | inductive call_ud (p: params) (globals: list ident): Type [0] ≝ |
---|
| 7 | | up: joint_internal_function p globals → call_ud p globals (* call *) |
---|
| 8 | | down: joint_internal_function p globals → call_ud p globals. (* return *) |
---|
| 9 | |
---|
| 10 | let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g)) |
---|
| 11 | (curr: nat) (max: nat) on fn_list: nat ≝ |
---|
| 12 | match fn_list with |
---|
| 13 | [ nil ⇒ max |
---|
| 14 | | cons h t ⇒ match h with |
---|
| 15 | [ up f ⇒ let new_stack ≝ curr + joint_if_stacksize … f in |
---|
| 16 | if leb max new_stack |
---|
| 17 | then max_stacksize … t new_stack new_stack |
---|
| 18 | else max_stacksize … t new_stack max |
---|
| 19 | | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in |
---|
| 20 | max_stacksize … t new_stack max |
---|
| 21 | ] |
---|
| 22 | ]. |
---|
| 23 | |
---|
| 24 | let rec extract_list_from_tlr (p: params) (g: list ident) |
---|
| 25 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 26 | (S: abstract_status) (s,s':S) (tr: trace_label_return S s s') |
---|
| 27 | (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ |
---|
| 28 | match tr with |
---|
| 29 | [ tlr_base s1 s2 tll ⇒ |
---|
| 30 | extract_list_from_tll … lg top_f … tll res |
---|
| 31 | | tlr_step s1 s2 s3 tll tlr ⇒ |
---|
| 32 | let res' ≝ extract_list_from_tll … lg top_f … tll res in |
---|
| 33 | extract_list_from_tlr … lg top_f … tlr res' |
---|
| 34 | ] |
---|
| 35 | and extract_list_from_tll (p: params) (g: list ident) |
---|
| 36 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 37 | (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s') |
---|
| 38 | (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ |
---|
| 39 | match tr with |
---|
| 40 | [ tll_base ends s1 s2 tal co ⇒ |
---|
| 41 | extract_list_from_tal … lg top_f … tal res |
---|
| 42 | ] |
---|
| 43 | and extract_list_from_tal (p: params) (g: list ident) |
---|
| 44 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 45 | (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s') |
---|
| 46 | (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ |
---|
| 47 | match tr with |
---|
| 48 | [ tal_base_not_return s1 s2 ex cl co ⇒ res |
---|
| 49 | | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res |
---|
[2426] | 50 | | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒ |
---|
| 51 | extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr |
---|
| 52 | (up ?? (lg (as_call_ident ? «s1p,cl»))::res) |
---|
| 53 | | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ |
---|
| 54 | let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr |
---|
| 55 | (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in |
---|
[2398] | 56 | extract_list_from_tal … lg top_f … tal res' |
---|
| 57 | | tal_step_default end s1p s1i s1e ex tal cl co ⇒ |
---|
| 58 | extract_list_from_tal … lg top_f … tal res |
---|
| 59 | ]. |
---|
| 60 | |
---|
| 61 | let rec tlr_rel_extract_equal (p: params) (g: list ident) |
---|
| 62 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 63 | S1 S2 s1 s1' s2 s2' t1 t2 on t1: |
---|
| 64 | tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → |
---|
| 65 | ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res = |
---|
| 66 | extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝ |
---|
| 67 | match t1 with |
---|
| 68 | [ tlr_base st1 st1' tll1 ⇒ ? |
---|
| 69 | | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? |
---|
| 70 | ] |
---|
| 71 | and tll_rel_extract_equal (p: params) (g: list ident) |
---|
| 72 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 73 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
---|
| 74 | t1 ≈ t2 → |
---|
| 75 | ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res = |
---|
| 76 | extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝ |
---|
| 77 | match t1 with |
---|
| 78 | [ tll_base ends st1 st1' tal1 co ⇒ ? |
---|
| 79 | ] |
---|
| 80 | and tal_rel_extract_equal (p: params) (g: list ident) |
---|
| 81 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 82 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
---|
| 83 | t1 ≈ t2 → |
---|
| 84 | ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res = |
---|
| 85 | extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝ |
---|
| 86 | match t1 with |
---|
| 87 | [ tal_base_not_return st1 st1' ex cl co ⇒ ? |
---|
| 88 | | tal_base_return st1 st1' ex cl ⇒ ? |
---|
[2426] | 89 | | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? |
---|
| 90 | | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? |
---|
[2398] | 91 | | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? |
---|
| 92 | ]. |
---|
| 93 | [ cases t2 |
---|
| 94 | [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim) |
---|
| 95 | | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs |
---|
| 96 | ] |
---|
| 97 | | cases t2 |
---|
| 98 | [ #st2 #st2' #tll2 normalize #abs cases abs |
---|
| 99 | | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res |
---|
| 100 | >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res) |
---|
| 101 | @(tlr_rel_extract_equal … (proj2 ?? Hsim)) |
---|
| 102 | ] |
---|
| 103 | | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2 |
---|
| 104 | @(tal_rel_extract_equal … H2) |
---|
| 105 | | cases t2 |
---|
| 106 | [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res % |
---|
| 107 | | #st2 #st2' #ex' #cl' * #abs destruct (abs) |
---|
[2426] | 108 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid * |
---|
[2398] | 109 | #taa * #H * #G * #K inversion taa in ⊢ ?; |
---|
| 110 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
---|
| 111 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
| 112 | normalize #abs destruct (abs) |
---|
| 113 | ] |
---|
[2426] | 114 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize * |
---|
[2398] | 115 | #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; |
---|
| 116 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
---|
| 117 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
| 118 | normalize #abs destruct (abs) |
---|
| 119 | ] |
---|
| 120 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa |
---|
| 121 | * #H * #G * #K inversion taa in ⊢ ?; |
---|
| 122 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
---|
| 123 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
[2426] | 124 | destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *) |
---|
| 125 | cases daemon |
---|
[2398] | 126 | ] |
---|
| 127 | ] |
---|
| 128 | | cases t2 |
---|
| 129 | [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs) |
---|
| 130 | | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % |
---|
[2426] | 131 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) |
---|
| 132 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 |
---|
[2398] | 133 | normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; |
---|
| 134 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
---|
| 135 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
| 136 | normalize #abs destruct (abs) |
---|
| 137 | ] |
---|
| 138 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid |
---|
| 139 | * #taa * #H * #G inversion taa in ⊢ ?; |
---|
| 140 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
---|
| 141 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
[2426] | 142 | destruct normalize #Hsim destruct (Hsim) |
---|
| 143 | cases daemon (* use Hind again? *) |
---|
[2398] | 144 | ] |
---|
| 145 | ] |
---|
| 146 | | cases t2 |
---|
[2426] | 147 | [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa |
---|
| 148 | * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1 |
---|
[2417] | 149 | [ * * #H3 #H2 #H4 | #H2 ] |
---|
| 150 | inversion taa in ⊢ ?; |
---|
| 151 | [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3) |
---|
| 152 | | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
| 153 | normalize in H3; destruct (H3) |
---|
| 154 | | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1) |
---|
| 155 | | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
[2398] | 156 | normalize in H1; destruct (H1) |
---|
| 157 | ] |
---|
| 158 | | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs) |
---|
[2426] | 159 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G |
---|
| 160 | * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L |
---|
| 161 | [* #tl2] |
---|
[2417] | 162 | inversion taa in ⊢ ?; |
---|
[2426] | 163 | [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
[2417] | 164 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
[2426] | 165 | destruct normalize * * #abs destruct (abs) |
---|
[2417] | 166 | | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res |
---|
[2426] | 167 | >(tlr_rel_extract_equal p g lg … H2) destruct (H1) |
---|
| 168 | >ident_eq % |
---|
[2398] | 169 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
| 170 | destruct normalize * #abs destruct (abs) |
---|
| 171 | ] |
---|
[2426] | 172 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize |
---|
| 173 | * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] |
---|
| 174 | #K * #tlr2' * #L [* #tl2] |
---|
[2398] | 175 | inversion taa in ⊢ ?; |
---|
[2426] | 176 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res |
---|
| 177 | destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq |
---|
| 178 | (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by |
---|
| 179 | * not sure yet *) cases daemon |
---|
| 180 | |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
| 181 | destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq |
---|
| 182 | >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *) |
---|
[2398] | 183 | ] |
---|
| 184 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * |
---|
[2426] | 185 | #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L |
---|
| 186 | [* #tl2] |
---|
[2417] | 187 | inversion taa in ⊢ ?; |
---|
[2426] | 188 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res |
---|
| 189 | destruct (H1) |
---|
| 190 | |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
| 191 | destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq |
---|
| 192 | >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *) |
---|
[2398] | 193 | ] |
---|
[2426] | 194 | ] |
---|
[2398] | 195 | | cases t2 |
---|
[2426] | 196 | [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa * |
---|
| 197 | #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2] |
---|
[2417] | 198 | inversion taa in ⊢ ?; |
---|
[2426] | 199 | [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1) |
---|
| 200 | |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
| 201 | destruct normalize * * #H1 destruct (H1) |
---|
| 202 | ] |
---|
| 203 | | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' |
---|
| 204 | * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2 |
---|
| 205 | inversion taa in ⊢ ?; |
---|
| 206 | [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
| 207 | | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
---|
[2398] | 208 | normalize * * #abs destruct (abs) |
---|
| 209 | ] |
---|
[2426] | 210 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G * |
---|
| 211 | #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L |
---|
| 212 | [2: * #tl2] |
---|
| 213 | inversion taa in ⊢ ?; |
---|
| 214 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res |
---|
| 215 | destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3) |
---|
| 216 | cases tal1 in H2; |
---|
| 217 | [ #ss #sf #ex'' #cl'' #co'' normalize #_ % |
---|
| 218 | | #ss #sf #ex'' #cl'' normalize #abs cases abs |
---|
| 219 | | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs |
---|
| 220 | | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1' |
---|
| 221 | normalize #abs cases abs |
---|
| 222 | | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize |
---|
| 223 | cases daemon (* use induction here, but no *) |
---|
[2417] | 224 | ] |
---|
[2426] | 225 | |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
[2417] | 226 | destruct normalize * * #abs destruct (abs) |
---|
[2398] | 227 | ] |
---|
[2426] | 228 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 |
---|
| 229 | normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * |
---|
| 230 | [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?; |
---|
| 231 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res |
---|
| 232 | destruct (H1) >ident_eq >(tal_rel_extract_equal … H2) |
---|
| 233 | >(tlr_rel_extract_equal … H3) % |
---|
| 234 | |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
[2398] | 235 | destruct normalize * * #abs destruct (abs) |
---|
| 236 | ] |
---|
[2426] | 237 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G * |
---|
| 238 | #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L |
---|
[2417] | 239 | [2: * #tl2] inversion taa in ⊢ ?; |
---|
[2426] | 240 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
---|
| 241 | |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
---|
| 242 | destruct normalize * * #H1 #H2 #H3 #res destruct (H1) |
---|
| 243 | >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon |
---|
| 244 | (* look further here *) |
---|
[2398] | 245 | ] |
---|
| 246 | ] |
---|
| 247 | | cases t2 |
---|
[2426] | 248 | [ #st2 #st2' #ex' #cl' #co' |
---|
| 249 | | #ss #fs #ex' #cl' |
---|
| 250 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' |
---|
| 251 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 |
---|
| 252 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' |
---|
[2398] | 253 | ] |
---|
[2426] | 254 | normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) |
---|
[2398] | 255 | ] |
---|
| 256 | qed. |
---|
| 257 | |
---|
[2456] | 258 | let rec tlr_rel_max_equal (p: params) (g: list ident) |
---|
[2398] | 259 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 260 | S1 S2 s1 s1' s2 s2' t1 t2 on t1: |
---|
| 261 | tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → |
---|
| 262 | max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) = |
---|
| 263 | max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝ |
---|
| 264 | match t1 with |
---|
| 265 | [ tlr_base st1 st1' tll1 ⇒ ? |
---|
| 266 | | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? |
---|
| 267 | ] |
---|
[2426] | 268 | and tll_rel_max_equal (p: params) (g: list ident) |
---|
[2398] | 269 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 270 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
---|
| 271 | t1 ≈ t2 → |
---|
| 272 | max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) = |
---|
| 273 | max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝ |
---|
| 274 | match t1 with |
---|
| 275 | [ tll_base ends st1 st1' tal1 co ⇒ ? |
---|
| 276 | ] |
---|
[2426] | 277 | and tal_rel_max_equal (p: params) (g: list ident) |
---|
[2398] | 278 | (lg: ident → joint_internal_function p g) (top_f: ident) |
---|
| 279 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
---|
| 280 | t1 ≈ t2 → |
---|
| 281 | max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) = |
---|
| 282 | max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝ |
---|
| 283 | match t1 with |
---|
| 284 | [ tal_base_not_return st1 st1' ex cl co ⇒ ? |
---|
| 285 | | tal_base_return st1 st1' ex cl ⇒ ? |
---|
[2456] | 286 | | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? |
---|
| 287 | | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? |
---|
[2398] | 288 | | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? |
---|
| 289 | ]. |
---|
[2456] | 290 | [1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) % |
---|
| 291 | |3: #Hsim >(tll_rel_extract_equal … Hsim []) % |
---|
| 292 | |*: #Hsim >(tal_rel_extract_equal … Hsim []) % |
---|
| 293 | ] |
---|
| 294 | qed. |
---|
[2398] | 295 | |
---|
| 296 | |
---|
| 297 | |
---|
| 298 | |
---|