Changeset 1877
 Timestamp:
 Apr 4, 2012, 6:48:27 PM (8 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.