Changeset 1877 for src/RTLabs/Traces.ma
- Timestamp:
- Apr 4, 2012, 6:48:27 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1812 r1877 55 55 | whd in H:(??%?); 56 56 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; 57 normalize try #a try #b try #c try #d try #e try #g try #h destruct57 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct 58 58 ] qed. 59 59 … … 511 511 [ @refl 512 512 | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %; 513 try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)513 try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct) 514 514 [ %1 %{A} %{B} %{C} @refl 515 515 | %2 %{A} %{B} @refl … … 565 565 * [ #f #fs #m whd in ⊢ (??%? → ?); 566 566 cases (lookup_present … (next f) (next_ok f)) normalize 567 try #A try #B try #C try #D try #E try #F try #G destruct567 try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct 568 568 | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl 569 569 | normalize #H411 #H412 #H413 #H414 #H415 destruct … … 582 582 cases fd 583 583 [ #fn whd in ⊢ (??%? → % → ?); 584 @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)584 @bind_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any) 585 585 #m' #b whd in ⊢ (??%? → ?); #E' destruct 586 586 * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 … … 682 682 [ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?); 683 683 cases (lookup_present ??? (next f) (next_ok f)) in E; 684 normalize #a try #b try #c try #d try #e try #f try #g destruct684 normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct 685 685 | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct 686 686 | #res #dst * … … 1178 1178 | St_const _ _ l ⇒ [l] 1179 1179 | St_op1 _ _ _ _ _ l ⇒ [l] 1180 | St_op2 _ _ _ _ l ⇒ [l]1180 | St_op2 _ _ _ _ _ _ _ l ⇒ [l] 1181 1181 | St_load _ _ _ l ⇒ [l] 1182 1182 | St_store _ _ _ l ⇒ [l] … … 1222 1222 | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1223 1223 | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1224 | # op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1224 | #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1225 1225 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1226 1226 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // … … 1314 1314 | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1315 1315 | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1316 | # op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl1316 | #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1317 1317 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1318 1318 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
Note: See TracChangeset
for help on using the changeset viewer.