Changeset 1707


Ignore:
Timestamp:
Feb 16, 2012, 6:05:57 PM (6 years ago)
Author:
campbell
Message:

Progress on finite segments of infinite RTLabs structured trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1706 r1707  
    7777| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
    7878| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
     79
     80coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
     81| nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H)
     82| nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr').
     83
     84lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'.
     85  not_wrong o i ge s (ft_step o i ge s tr s' H tr') →
     86  not_wrong o i ge s' tr'.
     87#o #i #ge #s #tr #s' #H #tr' #NW inversion NW
     88[ #H105 #H106 #H107 #H108 #H109 destruct
     89| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
     90] qed.
    7991
    8092let corec make_flat_trace ge s
     
    984996λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
    985997
    986 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
    987 | stlb_step : ∀l,n,H.
     998inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
     999| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
     1000| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
     1001with bound_on_steps_to_cost1 : label → nat → Prop ≝
     1002| bostc_step : ∀l,n,H.
    9881003    let stmt ≝ lookup_present … g l H in
    9891004    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
    990           (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
    991           steps_to_label_bound g l' n) →
    992     steps_to_label_bound g l (steps_for_statement stmt + n).
    993 
     1005          bound_on_steps_to_cost g l' n) →
     1006    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
     1007
     1008(*
    9941009lemma steps_to_label_bound_inv : ∀g,l,n.
    9951010  steps_to_label_bound g l n →
     
    10021017% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
    10031018qed.
    1004    
     1019  *) 
    10051020discriminator nat.
    1006 
     1021(*
    10071022definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
    10081023
     
    10201035| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
    10211036].
    1022 
    1023 definition frame_steps_to_label_bound : frame → nat → Prop ≝
    1024 λf. steps_to_label_bound (f_graph (func f)) (next f).
    1025 
    1026 inductive state_steps_to_label_bound : state → nat → Prop ≝
    1027 | sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n
    1028 | sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n)
    1029 | sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n)
     1037*)
     1038definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
     1039λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
     1040definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
     1041λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
     1042
     1043inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
     1044| sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n
     1045| sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n)
     1046| sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n)
    10301047.
    10311048
    1032 lemma state_steps_to_label_bound_zero : ∀s.
    1033   ¬ state_steps_to_label_bound s O.
     1049lemma state_bound_on_steps_to_cost_zero : ∀s.
     1050  ¬ state_bound_on_steps_to_cost s O.
    10341051#s % #H inversion H
    1035 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
    1036   inversion H52
    1037   #H68 #H69 #H70 #H71 #H72 #H73 #H74 normalize in H73; destruct
     1052[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
     1053  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
     1054  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
    10381055| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
    10391056| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
     
    10681085] qed.
    10691086
    1070 lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n.
    1071   state_steps_to_label_bound s (S n) →
     1087lemma bound_after_step : ∀ge,s,tr,s',n.
     1088  state_bound_on_steps_to_cost s (S n) →
    10721089  eval_statement ge s = Value ??? 〈tr, s'〉 →
    10731090  RTLabs_cost s' = false →
    10741091  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
    1075    state_steps_to_label_bound s' n.
    1076 #ge #s #tr #s' #n #STEPS inversion STEPS
     1092   state_bound_on_steps_to_cost s' n.
     1093#ge #s #tr #s' #n #BOUND1 inversion BOUND1
    10771094[ #f #fs #m #m #FS #E1 #E2 #_ destruct
    10781095  #EVAL cases (eval_successor … EVAL)
    10791096  [ /3/
    10801097  | * #l * #S1 #S2 #NC %2
    1081     cases (steps_to_label_bound_inv … FS ?) [2: @(next_ok f) ]
    1082     #n'
     1098  (*
     1099    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
     1100    *)
     1101    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
    10831102    inversion (eval_perserves … EVAL)
    1084     [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct
    1085       >(eval_steps … EVAL) * #En normalize in En;
    1086       #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
    1087       whd in S1:(??%?); destruct
    1088       %1 cases (H l S2)
    1089       [ * #LP
    1090         change with (RTLabs_cost (State (mk_frame H1 H7 l H9 H5 H6) fs' m')) in ⊢ (?% → ?);
    1091         >NC *
    1092       | //
     1103    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
     1104      >(eval_steps … EVAL) in E2; #En normalize in En;
     1105      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
     1106      %1 inversion (IH … S2)
     1107      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
     1108        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
     1109        whd in S1:(??%?); destruct >NC in CSx; *
     1110      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
    10931111      ]
    1094     | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
    1095       >(eval_steps … EVAL) * #En normalize in En;
    1096       #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
    1097       %2 whd lapply (H l S2)
    1098       @FS //
    1099     | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29
     1112    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
     1113      >(eval_steps … EVAL) in E2; #En normalize in En;
     1114      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
     1115      %2 @IH normalize in S1; destruct @S2
     1116    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
    11001117      destruct
    1101     | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
     1118    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
    11021119      normalize in S1; destruct
    1103     | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct
     1120    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
    11041121    ]
    11051122  ]
     
    11181135    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
    11191136    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
    1120     @FS
     1137    inversion FS
     1138    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
     1139        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
     1140        >NC in CSx; *
     1141    | #lx #nx #H #E1x #E2x #_ destruct @H
     1142    ]
    11211143  ]
    11221144] qed.
    11231145 
    1124 
    1125 (*
    1126 lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'.
    1127   state_steps_to_label_bound (State f fs m) (S (S n)) →
    1128   ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) →
    1129   eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    1130   state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]).
    1131 #ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H
    1132 [ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct
    1133   cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ]
    1134   #NC whd in ⊢ (??%? → ?);
    1135   generalize in ⊢ (??(?%)? → ?);
    1136   lapply (steps_to_label_bound_inv_step … H1 next_ok NC)
    1137   cases (lookup_present ??? next next_ok)
    1138   [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
    1139   | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
    1140   | #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
    1141   | #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
    1142   | #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
    1143   | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
    1144   | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
    1145   | #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
    1146   | #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
    1147   | #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
    1148   | #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    1149   | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    1150   | #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
    1151   | #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
    1152   ]
    1153 *)
    11541146(* When constructing an infinite trace, we need to be able to grab the finite
    11551147   portion of the trace for the next [trace_label_diverges] constructor.  We
     
    12081200  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    12091201  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
    1210   (LABEL_LIMIT: state_steps_to_label_bound s n)
     1202  (NOT_UNDEFINED: not_wrong … trace)
     1203  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
    12111204  on n : finite_prefix ge s ≝
    1212 match n return λn. state_steps_to_label_bound s n → finite_prefix ge s with
     1205match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
    12131206[ O ⇒ λLABEL_LIMIT. ⊥
    12141207| S n' ⇒
    1215     match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bound s (S n') → finite_prefix ge s with
    1216     [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
    1217     | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
     1208    match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
     1209    [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
     1210    | ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
    12181211        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    12191212        [ cl_other ⇒ λCL.
     
    12221215                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
    12231216            | false ⇒ λCS.
    1224                 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in
     1217                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ???? in
    12251218                fp_add_default ge ?? CL fs ? CS
    12261219            ] (refl ??)
    12271220        | cl_jump ⇒ λCL.
    12281221            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
    1229         | cl_call ⇒ λCL.?(*
     1222        | cl_call ⇒ λCL.
    12301223            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
    12311224            [ or_introl TERMINATES ⇒
     
    12341227                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
    12351228                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr)
    1236                 | false ⇒ λCS. ? (* broken - we don't know the new value of n *)
    1237                     (*let fs ≝ finite_segment ge (new_status … tlr) ??????????????
    1238                     fp_add_terminating_call … (new_trace … tlr) ? CS*)
     1229                | false ⇒ λCS.
     1230                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ???? in
     1231                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
    12391232                ] (refl ??)
    12401233              ]
    12411234            | or_intror NO_TERMINATION ⇒
    12421235                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
    1243             ]*)
     1236            ]
    12441237        | cl_return ⇒ λCL. ⊥
    12451238        ] (refl ??)
    1246     | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
    1247     ] STATE_COSTLABELLED NO_TERMINATION
     1239    | ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
     1240    ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION
    12481241] LABEL_LIMIT.
    1249 [ cases (state_steps_to_label_bound_zero s) /2/
     1242[ cases (state_bound_on_steps_to_cost_zero s) /2/
    12501243| (* TODO: how do we know that we're not at the final state? *)
    12511244| @(absurd ?? NO_TERMINATION)
    12521245     %{0} % @wr_base //
    12531246| @(well_cost_labelled_jump … EV) //
    1254 | 5,6,8,9,10: /2/
    1255 |
     1247| 5,6,7,8,9,10: /2/
     1248| /2/
     1249| //
     1250| (* FIXME: post-call non-termination *)
     1251| (* FIXME: post-call not-wrong *)
     1252| (* FIXME: bound on steps after call *)
     1253| @(well_cost_labelled_state_step … EV) //
     1254| @(well_cost_labelled_call … EV) //
     1255| 18,19,20: /2/
    12561256| @(well_cost_labelled_state_step … EV) //
    12571257| @(not_to_not … NO_TERMINATION)
    12581258  * #depth * #TERM %{depth} % @wr_step /2/
    1259 | cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?)
    1260 
    1261 @(well_cost_labelled_call … EV) //
    1262 |
    1263  2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
    1264 | 5,6,8: /2/
    1265 |
    1266 |*)
    1267 | 12,13,14: /2/
    1268 | @(well_cost_labelled_state_step … EV) //
    1269 | @(not_to_not … NO_TERMINATION)
    1270   * #depth * #TERM %{depth} % @wr_step /2/
     1259| @(still_not_wrong … NOT_UNDEFINED)
     1260| cases (bound_after_step … LABEL_LIMIT EV ?)
     1261  [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 // |
     1262    inversion trace'
     1263    [ cases daemon (* TODO again *) | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct
     1264    @wr_base //
     1265    | #H99 #H100 #H101 #H102 #H103 destruct
     1266      inversion NOT_UNDEFINED
     1267      [ #H137 #H138 #H139 #H140 #H141 destruct
     1268      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct
     1269        inversion H148
     1270        [ #H153 #H154 #H155 #H156 #H157 destruct
     1271        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
     1272        ]
     1273      ]
     1274    ]
     1275    ]
     1276    | >CL #E destruct
     1277    ]
     1278  | //
     1279  | //
     1280  ]
     1281| inversion NOT_UNDEFINED
     1282  [ #H169 #H170 #H171 #H172 #H173 destruct
     1283  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
     1284  ]
    12711285] cases daemon qed.
    12721286
Note: See TracChangeset for help on using the changeset viewer.