Changeset 1596


Ignore:
Timestamp:
Dec 7, 2011, 4:24:42 PM (8 years ago)
Author:
campbell
Message:

RTLabs structured traces: sort out passing of termination proofs around.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1595 r1596  
    243243] qed.
    244244
    245 (*
    246 (* If we'll return then we must return from calls. *)
    247 lemma will_return_call : ∀ge,depth,s,trace.
    248   will_return ge (S depth) s trace →
    249   will_return ge depth s trace.
    250 #ge #depth #s #trace #H elim H in ⊢ ?;
    251 [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
    252 | #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
    253 | #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/
    254 | #H215 #H216 #H217 #H218 #H219 #H220 #H221
    255   inversion H221
    256   [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct
    257   | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct
    258   | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct
    259   | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct
    260 ] qed. check will_return_call.
    261 | #H130 #H131 #H132 #H133 #H134 #H135
    262   inversion H
    263   [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct
    264     cases H196 #E destruct
    265  
    266 
    267 let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace)
    268   on H : will_return ge depth s trace ≝
    269 match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with
    270 [ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ?
    271 | wr_call s tr s' d EX trace CL H' ⇒ λE. ?
    272 | wr_ret s tr s' d EX trace CL H' ⇒ λE. ?
    273 | wr_base s tr s' EX trace CL ⇒ λE. ?
    274 ] (refl ? (S depth)).
    275 [ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H')
    276   @(will_return_call … H'')
    277 | *: cases daemon ] qed.
    278 | %2 /2/
    279 | destruct cases d in H' ⊢ %;
    280   [ #H' @wr_base //
    281   | #d' #H' %3 /2/
    282   ]
    283 | destruct
    284 ] qed.
    285 
    286 (* If we'll return then we must return from calls. *)
    287 lemma will_return_call : ∀ge,depth,s,trace.
    288   will_return ge (S depth) s trace →
    289   will_return ge depth s trace.
    290 #ge #depth #s #trace #H lapply (refl ? (S depth))
    291 generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %);
    292 [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/
    293 | #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3
    294  
    295 discriminator nat.
    296 
    297 
    298 
    299 (* Find time until a nested call completes. *)
    300 lemma nth_is_return_down : ∀ge,n,depth,s,trace.
    301   nth_is_return ge n (S depth) s trace →
    302   ∃m. nth_is_return ge m depth s trace.
    303 #ge #n elim n
    304 (* It's impossible to run out of time... *)
    305 [ #depth #s #trace #H inversion H
    306   [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
    307   | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
    308   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
    309   | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
    310   ]
    311 | #n' #IH #depth #s #trace #H inversion H
    312   [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    313     cases (IH depth s1' trace1 ?)
    314     [ #m' #H' %{(S m')} %1 //
    315     | //
    316     ]
    317   | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    318     cases (IH (S depth) s1' trace1 ?)
    319     [ #m' #H' %{(S m')} %2 //
    320     | //
    321     ]
    322   | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    323     cases (depth1) in H2 ⊢ %;
    324     [ #H2 %{O} %4 //
    325     | #depth' #H2 cases (IH depth' s1' trace1 ?)
    326       [ #m' #H' %{(S m')} %3 //
    327       | //
    328       ]
    329     ]
    330   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
    331   ]
    332 ] qed.
    333 
    334 lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
    335   RTLabs_classify s = cl_call →
    336   nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
    337   ∃m. nth_is_return ge m O s' trace.
    338 #ge #n #s #tr #s' #EX #trace #CLASS #H
    339 inversion H
    340 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
    341   -H2 destruct >H1 in CLASS; #E destruct
    342 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
    343   @nth_is_return_down //
    344 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
    345   -H2 destruct
    346 | #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
    347 ] qed.
    348 
    349 lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace.
     245
     246lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
    350247  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
    351   nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
    352   nth_is_return ge (pred n) O s' trace.
    353 #ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM
    354 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
    355 | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct
    356 | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
    357 | #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct
    358 | #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct //
    359 | #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct
    360 | #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
    361 | #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
    362 ] qed.
    363 *)
    364 
    365 lemma will_return_notfn : ∀ge,s,tr,s',EX,trace.
    366   RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
    367   will_return ge O s (ft_step ?? ge s tr s' EX trace) →
    368   will_return ge O s' trace.
    369 #ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM
     248  will_return ge d s (ft_step ?? ge s tr s' EX trace) →
     249  will_return ge d s' trace.
     250#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
    370251[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
    371252| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
    372 | #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct
     253| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct >CL in H324; #E destruct
    373254| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
    374255| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
    375256| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
    376 | #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct
     257| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct >CL in H377; #E destruct
    377258| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
    378259] qed.
     
    522403(* Don't need to know that labels break loops because we have termination. *)
    523404
    524 record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
     405(* A bit of mucking around with the depth to avoid proving termination after
     406  termination. *)
     407record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) : Type[0] ≝ {
    525408  new_state : state;
    526409  remainder : flat_trace io_out io_in ge new_state;
    527410  cost_labelled : well_cost_labelled_state new_state;
    528   new_trace : T new_state
     411  new_trace : T new_state;
     412  terminates : match depth with
     413               [ O ⇒ True
     414               | S d ⇒ will_return ge d new_state remainder
     415               ]
    529416}.
    530417
    531 record sub_trace_result (ge:genv) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
     418record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
    532419  ends : trace_ends_with_ret;
    533   trace_res :> trace_result ge (T ends);
    534   terminates :
    535     (* We handle returns specially *)
    536     match ends with
    537     [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res)
    538     | ends_with_ret ⇒ True
    539     ]
     420  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends)
    540421}.
    541422
    542 definition replace_sub_trace : ∀ge,T1,T2.
    543   ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝
    544 λge,T1,T2,r,trace.
    545   mk_sub_trace_result ge T2
     423definition replace_sub_trace : ∀ge,trm,T1,T2.
     424  ∀r:sub_trace_result ge trm T1. T2 (ends … r) (new_state … r) → sub_trace_result ge trm T2 ≝
     425λge,trm,T1,T2,r,trace.
     426  mk_sub_trace_result ge trm T2
    546427    (ends … r)
    547     (mk_trace_result ge (T2 (ends … r))
     428    (mk_trace_result ge ? (T2 (ends … r))
    548429      (new_state … r)
    549430      (remainder … r)
    550431      (cost_labelled … r)
    551432      trace
     433      (terminates … r)
    552434    )
    553     (terminates … r)
    554435.
    555436
    556 definition replace_trace : ∀ge,T1,T2.
    557   ∀r:trace_result ge T1. T2 (new_state … r) → trace_result ge T2 ≝
    558 λge,T1,T2,r,trace.
    559   mk_trace_result ge T2
     437definition replace_trace : ∀ge,trm,T1,T2.
     438  ∀r:trace_result ge trm T1. T2 (new_state … r) → trace_result ge trm T2 ≝
     439λge,trm,T1,T2,r,trace.
     440  mk_trace_result ge trm T2
    560441    (new_state … r)
    561442    (remainder … r)
    562443    (cost_labelled … r)
    563444    trace
     445    (terminates … r)
    564446.
    565447
    566 let rec make_label_return ge s
     448let rec make_label_return ge depth s
    567449  (trace: flat_trace io_out io_in ge s)
    568450  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    569451  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    570452  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    571   (TERMINATES: will_return ge O s trace)
    572   : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝
    573 
    574   let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
    575   match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with
    576   [ ends_with_ret ⇒ λtll,term.
    577       replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
    578   | doesnt_end_with_ret ⇒ λtll,term.
    579       let r' ≝ make_label_return ge (new_state … r)
    580                  (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? term in
     453  (TERMINATES: will_return ge depth s trace)
     454  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) ≝
     455
     456  let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
     457  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) → ? with
     458  [ ends_with_ret ⇒ λr.
     459      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
     460  | doesnt_end_with_ret ⇒ λr.
     461      let r' ≝ make_label_return ge depth (new_state … r)
     462                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (terminates ??? r) in
    581463        replace_trace … r'
    582           (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
    583   ] (new_trace … r) (terminates … r)
    584 
    585 and make_label_label ge s
     464          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r'))
     465  ] (trace_res … r)
     466
     467and make_label_label ge depth s
    586468  (trace: flat_trace io_out io_in ge s)
    587469  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    588470  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    589471  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    590   (TERMINATES: will_return ge O s trace)
    591   : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝
    592 let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
    593   replace_sub_trace ??? r
     472  (TERMINATES: will_return ge depth s trace)
     473  : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) ≝
     474let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
     475  replace_sub_trace r
    594476    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
    595477
    596 and make_any_label ge s
     478and make_any_label ge depth s
    597479  (trace: flat_trace io_out io_in ge s)
    598480  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    599481  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    600   (TERMINATES: will_return ge O s trace)
    601   : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝
    602 match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with
     482  (TERMINATES: will_return ge depth s trace)
     483  : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) ≝
     484match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) with
    603485[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
    604486| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
     
    607489        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    608490        [ true ⇒ λCS.
    609             mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
     491            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
     492              doesnt_end_with_ret
     493              (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
    610494        | false ⇒ λCS.
    611             let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in
    612                 replace_sub_trace ??? r
     495            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? in
     496                replace_sub_trace r
    613497                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
    614498        ] (refl ??)
    615499    | cl_jump ⇒ λCL.
    616         mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
     500        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
     501          doesnt_end_with_ret
     502          (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
    617503    | cl_call ⇒ λCL.
    618         let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in
    619         let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
    620         replace_sub_trace ??? r'
     504        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? in
     505        let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
     506        replace_sub_trace ???? r'
    621507          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
    622508    | cl_return ⇒ λCL.
    623         mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?
     509        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
     510          ends_with_ret
     511          (mk_trace_result ge ??
     512            next
     513            trace'
     514            ?
     515            (tal_base_return (RTLabs_status ge) start next ? CL)
     516            ?)
    624517    ] (refl ? (RTLabs_classify start))
    625518| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
    626519] STATE_COSTLABELLED TERMINATES.
    627520
    628 [ @(trace_label_label_label … tll)
     521[ @(trace_label_label_label … (new_trace … r))
    629522|
     523| inversion TERMINATES
     524  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct >CL in H7; * #E destruct
     525  | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 -TERMINATES destruct >CL in H21; #E destruct
     526  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 -TERMINATES destruct @H36
     527  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 whd @I
     528  ]
    630529| %{tr} @EV
    631530| @(well_cost_labelled_state_step  … EV) //
    632 | @I
     531| whd @(will_return_notfn … TERMINATES) %2 @CL
    633532| %{tr} @EV
    634533| % whd in ⊢ (% → ?); >CL #E destruct
    635534| @(well_cost_labelled_jump … EV) //
    636535| @(well_cost_labelled_state_step  … EV) //
    637 | @(will_return_notfn … TERMINATES) %2 @CL
    638536| (* oh dear *)
    639537| %{tr} @EV
    640538| @(cost_labelled … r)
    641 |
    642 |
    643 |
    644 
    645  @(well_cost_labelled_state_step  … EV) //
     539| @(terminates … r)
     540| @(well_cost_labelled_state_step  … EV) //
     541| @(well_cost_labelled_call … EV) //
     542| inversion TERMINATES
     543  [ #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 -TERMINATES destruct >CL in H60; * #E destruct
     544  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 -TERMINATES destruct @H75
     545  | #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 -TERMINATES destruct >CL in H88; #E destruct
     546  | #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 -TERMINATES destruct >CL in H101; #E destruct
     547  ]
     548| whd @(will_return_notfn … TERMINATES) %1 @CL
     549| %{tr} @EV
    646550| % whd in ⊢ (% → ?); >CL #E destruct
    647551| @CS
    648 | @(nth_is_return_notfn … TERMINATES) %1 @CL
     552| @(well_cost_labelled_state_step  … EV) //
    649553| % whd in ⊢ (% → ?); >CS #E destruct
    650554| @CL
    651555| %{tr} @EV
    652556| @(well_cost_labelled_state_step  … EV) //
    653 | @(nth_is_return_notfn … TERMINATES) %1 @CL
     557| @(will_return_notfn … TERMINATES) %1 @CL
    654558| inversion TERMINATES
    655   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
    656   | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
    657   | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
    658   | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
     559  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct
     560  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES destruct
     561  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES destruct
     562  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES destruct
    659563  ]
    660564|
Note: See TracChangeset for help on using the changeset viewer.