Changeset 2840
- Timestamp:
- Mar 11, 2013, 12:18:26 PM (5 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabs_partial_traces.ma
r2839 r2840 107 107 qed. 108 108 109 (* Need a way to choose whether a called function terminates. Then,110 if the initial function terminates we generate a purely inductive structured trace,111 otherwise we start generating the coinductive one, and on every function call112 use the choice method again to decide whether to step over or keep going.113 114 Not quite what we need - have to decide on seeing each label whether we will see115 another or hit a non-terminating call?116 117 Also - need the notion of well-labelled in order to break loops.118 119 120 121 outline:122 123 does function terminate?124 - yes, get (bound on the number of steps until return), generate finite125 structure using bound as termination witness126 - no, get (¬ bound on steps to return), start building infinite trace out of127 finite steps. At calls, check for termination, generate appr. form.128 129 generating the finite parts:130 131 We start with the status after the call has been executed; well-labelling tells132 us that this is a labelled state. Now we want to generate a trace_label_return133 and also return the remainder of the flat trace.134 135 *)136 109 137 110 (* [will_return ge depth s trace] says that after a finite number of steps of … … 1009 982 *) 1010 983 1011 inductive inhabited (T:Type[0]) : Prop ≝1012 | witness : T → inhabited T.1013 984 1014 985 … … 1322 1293 ] qed. 1323 1294 1324 (* When constructing an infinite trace, we need to be able to grab the finite1325 portion of the trace for the next [trace_label_diverges] constructor. We1326 use the fact that the trace is soundly labelled to achieve this. *)1327 1328 record remainder_ok (ge:genv) (s:RTLabs_ext_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {1329 ro_well_cost_labelled: well_cost_labelled_state s;1330 ro_soundly_labelled: soundly_labelled_state s;1331 ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));1332 ro_not_final: RTLabs_is_final s = None ?1333 }.1334 1335 inductive finite_prefix (ge:genv) : RTLabs_ext_state ge → Prop ≝1336 | fp_tal : ∀s,s':RTLabs_ext_state ge.1337 trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →1338 ∀t:flat_trace io_out io_in ge s'.1339 remainder_ok ge s' t →1340 finite_prefix ge s1341 | fp_tac : ∀s1,s2,s3:RTLabs_ext_state ge.1342 trace_any_call (RTLabs_status ge) s1 s2 →1343 well_cost_labelled_state s2 →1344 as_execute (RTLabs_status ge) s2 s3 →1345 ∀t:flat_trace io_out io_in ge s3.1346 remainder_ok ge s3 t →1347 finite_prefix ge s11348 .1349 1350 definition fp_add_default : ∀ge. ∀s,s':RTLabs_ext_state ge.1351 RTLabs_classify s = cl_other →1352 finite_prefix ge s' →1353 as_execute (RTLabs_status ge) s s' →1354 RTLabs_cost s' = false →1355 finite_prefix ge s ≝1356 λge,s,s',OTHER,fp.1357 match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with1358 [ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf1359 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))1360 rem rok1361 | fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s31362 (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))1363 WCL2 EV rem rok1364 ].1365 1366 definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ext_state ge.1367 as_execute (RTLabs_status ge) s s1 →1368 ∀CALL:RTLabs_classify s = cl_call.1369 finite_prefix ge s'' →1370 trace_label_return (RTLabs_status ge) s1 s'' →1371 as_after_return (RTLabs_status ge) «s, CALL» s'' →1372 RTLabs_cost s'' = false →1373 finite_prefix ge s ≝1374 λge,s,s1,s'',EVAL,CALL,fp.1375 match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with1376 [ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf1377 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)1378 rem rok1379 | fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s31380 (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)1381 WCL2 EV rem rok1382 ].1383 1384 lemma not_return_to_not_final : ∀ge,s,tr,s'.1385 eval_statement ge s = Value ??? 〈tr, s'〉 →1386 RTLabs_classify s ≠ cl_return →1387 RTLabs_is_final s' = None ?.1388 #ge #s #tr #s' #EV1389 inversion (eval_preserves … EV) //1390 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL1391 @⊥ @(absurd ?? CL) @refl1392 qed.1393 (*1394 definition termination_oracle ≝ ∀ge,depth,s,trace.1395 inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).1396 1397 let rec finite_segment ge (s:RTLabs_ext_state ge) n trace1398 (ORACLE: termination_oracle)1399 (TRACE_OK: remainder_ok ge s trace)1400 (ENV_COSTLABELLED: well_cost_labelled_ge ge)1401 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)1402 (LABEL_LIMIT: state_bound_on_steps_to_cost s n)1403 on n : finite_prefix ge s ≝1404 match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with1405 [ O ⇒ λLABEL_LIMIT. ⊥1406 | S n' ⇒1407 match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace'.1408 match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_ext_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_ext_state ge s ? mtc) with1409 [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥1410 | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.1411 let start' ≝ mk_RTLabs_ext_state ge start stk mtc in1412 let next' ≝ next_state ge start' next tr EV in1413 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with1414 [ cl_other ⇒ λCL.1415 let TRACE_OK' ≝ ? in1416 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with1417 [ true ⇒ λCS.1418 fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'1419 | false ⇒ λCS.1420 let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in1421 fp_add_default ge start' next' CL fs ? CS1422 ] (refl ??)1423 | cl_jump ⇒ λCL.1424 fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?1425 | cl_call ⇒ λCL.1426 match ORACLE ge O next trace' return λ_. finite_prefix ge start' with1427 [ or_introl TERMINATES ⇒1428 match TERMINATES with [ witness TERMINATES ⇒1429 let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in1430 let TRACE_OK' ≝ ? in1431 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with1432 [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? (CL) ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'1433 | false ⇒ λCS.1434 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in1435 fp_add_terminating_call … fs (new_trace … tlr) ? CS1436 ] (refl ??)1437 ]1438 | or_intror NO_TERMINATION ⇒1439 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (CL))) ?? trace' ?1440 ]1441 | cl_return ⇒ λCL. ⊥1442 | cl_tailcall ⇒ λCL. ⊥1443 ] (refl ??)1444 ] mtc01445 ] trace TRACE_OK1446 ] LABEL_LIMIT.1447 [ cases (state_bound_on_steps_to_cost_zero s) /2/1448 | @(absurd … (ro_not_final … TRACE_OK) FINAL)1449 | @(absurd ?? (ro_no_termination … TRACE_OK))1450 %{0} % @wr_base //1451 | @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]1452 | %1 @(CL)1453 | 6,9,10,11: /3/1454 | cases TRACE_OK #H1 #H2 #H3 #H41455 % [ @(well_cost_labelled_state_step … EV) //1456 | @(soundly_labelled_state_step … EV) //1457 | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/1458 | @(not_return_to_not_final … EV) >CL % #E destruct1459 ]1460 | @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //1461 | @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //1462 | @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)1463 @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //1464 | % [ /2/1465 | @(soundly_labelled_state_preserved … (stack_ok … tlr))1466 @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)1467 | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %1468 @wr_call //1469 @(will_return_prepend … TERMINATES … TM1)1470 cases (terminates … tlr) //1471 | (* By stack preservation we cannot be in the final state *)1472 inversion (stack_ok … tlr)1473 [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct1474 | #s1 #f #f' #fs #m #fn #S #M #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl1475 | #s1 #r #M #S #E1 #E2 #E3 #E4 change with (next_state ?????) in E2:(??%??); -TERMINATES destruct -next' -s01476 cases (rtlabs_call_inv … CL) #vf * #fd * #args * #dst * #stk * #m #E destruct1477 inversion (eval_preserves … EV)1478 [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 try #H124 @⊥ -next destruct ]1479 #ge' #vf' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct1480 inversion S1481 [ #f #fs0 #m #fn0 #S0 #M0 #E1 #E2 whd in ⊢ (??%?% → ?); generalize in ⊢ (??(????%)?? → ?); #M'' #E3 #_ destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H1 #H2 #H3 try #H130 try #H4 try #H5 try #H6 [ whd in H6:(??%?%); | whd in H2:(??%?%); ] destruct ]1482 (* state_bound_on_steps_to_cost needs to know about the current stack frame,1483 so we can use it as a witness that at least one frame exists *)1484 inversion LABEL_LIMIT1485 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 try #H151 destruct1486 | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 destruct1487 ]1488 ]1489 | @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)1490 | @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]1491 | /2/1492 | %{tr} %{EV} %1493 | cases TRACE_OK #H1 #H2 #H3 #H41494 % [ @(well_cost_labelled_state_step … EV) /2/1495 | @(soundly_labelled_state_step … EV) /2/1496 | @(not_to_not … NO_TERMINATION) * #depth * #TM %1497 @(will_return_lower … TM) //1498 | @(not_return_to_not_final … EV) >CL % #E destruct1499 ]1500 | @(RTLabs_notail … CL)1501 | %2 @(CL)1502 | 21,22: %{tr} %{EV} %1503 | cases (bound_after_step … LABEL_LIMIT EV ?)1504 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |1505 inversion trace'1506 [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥1507 @(absurd ?? FINAL) @(not_return_to_not_final … EV)1508 % >CL #E destruct1509 | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct1510 @wr_base //1511 ]1512 ]1513 | >CL #E destruct1514 ]1515 | //1516 | //1517 ]1518 | cases (bound_after_step … LABEL_LIMIT EV ?)1519 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |1520 inversion trace'1521 [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥1522 @(absurd ?? FINAL) @(not_return_to_not_final … EV)1523 % >CL #E destruct1524 | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct1525 @wr_base //1526 ]1527 ]1528 | >CL #E destruct1529 ]1530 | //1531 | //1532 ]1533 | cases TRACE_OK #H1 #H2 #H3 #H41534 % [ @(well_cost_labelled_state_step … EV) //1535 | @(soundly_labelled_state_step … EV) //1536 | @(not_to_not … (ro_no_termination … TRACE_OK))1537 * #depth * #TERM %{depth} % @wr_step /2/1538 | @(not_return_to_not_final … EV) >CL % #E destruct1539 ]1540 ] qed.1541 *)1542 1295 lemma simplify_cl : ∀ge,s,c. 1543 1296 as_classifier (RTLabs_status ge) s c → … … 1891 1644 [ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac 1892 1645 ] EX''. 1893 (*1894 (* Now reconstruct the flat_trace of a diverging execution. Note that we need1895 to take care to satisfy the guardedness condition by witnessing the fact that1896 the partial traces are non-empty. *)1897 let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge)1898 (tr:trace_label_diverges (RTLabs_status ge) s)1899 : flat_trace io_out io_in ge s ≝1900 match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with1901 [ tld_step sx sy tll tld ⇒1902 match sy in RTLabs_ext_state return λsy:RTLabs_ext_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state sy' stk mtc0 ⇒1903 λtll.1904 match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s2 stk mtc) → flat_trace ??? s1 with1905 [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)1906 | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)1907 ] mtc0 ] tll tld1908 | tld_base s1 s2 s3 tlc EX CL tld ⇒1909 match s3 in RTLabs_ext_state return λs3:RTLabs_ext_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state s3' stk mtc0 ⇒1910 λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒1911 match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s3 stk mtc) → flat_trace ??? s1 with1912 [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)1913 | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)1914 ] mtc01915 ]1916 ] EX tld1917 ]1918 (* Helper to keep adding the partial trace without violating the guardedness1919 condition. *)1920 and add_partial_flat_trace ge (s:state) (s':RTLabs_ext_state ge)1921 : partial_flat_trace io_out io_in ge s s' →1922 trace_label_diverges (RTLabs_status ge) s' →1923 flat_trace io_out io_in ge s ≝1924 match s' return λs':RTLabs_ext_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_ext_state sx stk mtc ⇒1925 λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s' ? mtc) → flat_trace io_out io_in ge s with1926 [ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)1927 | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_ext_state ge s3 stk mtc) tr' tr)1928 ] mtc ]1929 .1930 1931 1932 coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝1933 | eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)1934 | eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2).1935 1936 let corec flat_traces_are_determined_by_starting_point ge s tr11937 : ∀tr2. equal_flat_traces ge s tr1 tr2 ≝1938 match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with1939 [ ft_stop s F ⇒ λtr2. ?1940 | ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.1941 match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with1942 [ ft_stop s F ⇒ λEX. ?1943 | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?1944 ] EX01945 ].1946 [ inversion tr2 in tr1 F;1947 [ #s #F #_ #_ #tr1 #F' @eft_stop1948 | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct1949 cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct1950 ]1951 | @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct1952 | -EX01953 cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)1954 @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')1955 -E -EX' -tr2' #tr2' #EX'1956 cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)1957 @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')1958 -E -EX' #EX'1959 @eft_step @flat_traces_are_determined_by_starting_point1960 ] qed.1961 1962 let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)1963 (str:trace_label_diverges (RTLabs_status ge) s)1964 (tr:flat_trace io_out io_in ge s)1965 : equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.1966 @flat_traces_are_determined_by_starting_point1967 qed.1968 1969 let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge)1970 (tr:trace_whole_program (RTLabs_status ge) s)1971 on tr : flat_trace io_out io_in ge s ≝1972 match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with1973 [ twp_terminating s1 s2 sf CL EX tlr F ⇒1974 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒1975 ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))1976 ]1977 | twp_diverges s1 s2 CL EX tld ⇒1978 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒1979 ft_step … EX' (flat_trace_of_label_diverges … tld)1980 ]1981 ].1982 1983 let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)1984 (str:trace_whole_program (RTLabs_status ge) s)1985 (tr:flat_trace io_out io_in ge s)1986 : equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.1987 @flat_traces_are_determined_by_starting_point1988 qed.1989 *)1990 1646 1991 1647
Note: See TracChangeset
for help on using the changeset viewer.