Ignore:
Timestamp:
May 8, 2012, 3:41:43 PM (8 years ago)
Author:
campbell
Message:

Main labelling simulation proof complete.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r1920 r1922  
    322322qed.
    323323
    324 inductive state_with_labels : state → state → Prop ≝
    325 | swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
     324inductive state_with_labels_partial : state → state → Prop ≝
     325| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
    326326(* Extra matching states that we can reach that don't quite correspond to the
    327327   labelling function *)
    328328| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    329     state_with_labels (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     329    state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    330330| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    331     state_with_labels (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     331    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
    332332| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    333     state_with_labels (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     333    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
     334(* and the rest *)
     335| swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
     336| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
     337| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
     338.
     339
     340(* We handle the switch states after the rest so that we can reuse the partial
     341   result. *)
     342inductive state_with_labels : state → state → Prop ≝
     343| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
    334344| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
    335345    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
    336346                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
    337 (* and the rest *)
    338 | swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
    339 | swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels (Returnstate res k m) (Returnstate res k' m)
    340 | swl_finalstate : ∀r. state_with_labels (Finalstate r) (Finalstate r)
    341347.
    342348
     
    550556     ]
    551557] qed.
     558
     559lemma label_fn_params : ∀f.
     560  fn_params (label_function f) = fn_params f.
     561* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
     562qed.
     563
     564lemma label_fn_vars : ∀f.
     565  fn_vars (label_function f) = fn_vars f.
     566* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
     567qed.
    552568
    553569(* Apply induction hypothesis while getting Matita to infer the continuations
     
    731747qed.
    732748
    733 lemma step_with_labels : ∀ge,ge'.
     749(* We show the main simulation in two stages.  First, we show it for all states
     750   in the relation *except* those for labeled_statements, then we'll show the
     751   whole thing.  This is so that we can appeal to the other cases in the proof
     752   for labeled_statements. *)
     753lemma step_with_labels_partial : ∀ge,ge'.
    734754  related_globals ge ge' →
    735755  ∀s1,s1',tr,s2.
    736   state_with_labels s1 s1' →
     756  state_with_labels_partial s1 s1' →
    737757  exec_step ge s1 = Value … 〈tr,s2〉 →
    738   ∃tr',s2'. plus ge' s1' tr' s2' ∧
    739             trace_with_extra_labels tr tr' ∧
    740             state_with_labels s2 s2'.
     758   ∃tr',s2'. plus ge' s1' tr' s2' ∧
     759             trace_with_extra_labels tr tr' ∧
     760             state_with_labels s2 s2'.
    741761#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
    742762[ #f #us #s #k #k' #e #m #KL cases s
     
    747767      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list ? m (blocks_of_env e)))}
    748768        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    749         | // ] | /2/ ]
     769        | // ] | /3/ ]
    750770      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
    751771      ]
     
    753773      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
    754774      whd in EX:(??%%); destruct
    755       % [ % [ @plus_one @refl | // ] | /2/ ]
     775      % [ % [ @plus_one @refl | // ] | /3/ ]
    756776    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
    757777      whd in EX:(??%%); destruct
    758       % [ 2: % [ % [ @plus_one @refl | // ] | @swl_whilestate // ] | skip ]
     778      % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
    759779    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    760780      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
     
    767787        whd in ⊢ (??%?); @refl
    768788        | // ]
    769         | @swl_dowhilestate // ] | skip ] | skip ]
     789        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
    770790      | % [ 2: % [ 2: % [ % [ @plus_succ [
    771791        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
     
    776796        | 5: @plus_one @refl | skip ] | skip ]
    777797        | <(E0_right tr) @twel_app /2/ ]
    778         | /2/ ] | skip ] | skip ]
     798        | /3/ ] | skip ] | skip ]
    779799      ]
    780800    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
     
    783803    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    784804      whd in EX:(??%?); destruct
    785       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     805      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
    786806    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    787807      whd in EX:(??%?); destruct
    788       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     808      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
    789809    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    790810      whd in EX:(??%?); destruct
    791       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     811      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
    792812    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    793813      whd in EX:(??%?);
     
    795815      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
    796816        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    797         @refl | // ] | /3/ ] | skip ]
     817        @refl | // ] | /4/ ] | skip ]
    798818      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
    799819      ]
    800820    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    801       % [2: % [2: % [ % [ @plus_one @refl | // ] | /2/ ]| skip ]| skip ]
     821      % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
    802822    ]
    803823  | * #a1 #ty1 #a2 #EX
     
    816836      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
    817837      @refl
    818     | @twel_app // ] | /2/ ] | skip ] | skip ]
     838    | @twel_app // ] | /3/ ] | skip ] | skip ]
    819839  | * [2: * #er #tyr ] #ef #args #EX
    820840    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    839859      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
    840860      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
    841       @refl | *: @twel_app /2/ ] | *: @swl_callstate /2/ ] | *: skip ] | *: skip ]
     861      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
    842862  | #st1 #st2 #EX
    843863    whd in EX:(??%%); destruct
    844864    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    845     %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_state /2/ ] | skip ]
     865    %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
    846866  | #a #st1 #st2 #EX
    847867    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    863883    ]
    864884    | 2,4: <(E0_right tr) @twel_app /2/
    865     ]| 2,4: /2/ ] | *: skip ] | *: skip ]
     885    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
    866886  | #a #st #EX
    867887    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    885905    ]
    886906    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
    887     ]| 2,4: /3/ ] | *: skip ] | *: skip ]
     907    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
    888908  | #a #st #EX
    889909    normalize in EX; destruct
     
    894914    % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
    895915      | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
    896       | /2/ ] | /3/ ] | skip ] | skip ]
     916      | /2/ ] | /4/ ] | skip ] | skip ]
    897917  | #st1 #a #st2 #st #EX
    898918    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
     
    917937      ]
    918938      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
    919       ]| 2,4: /3/ ] | *: skip ] | *: skip ]
     939      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
    920940    | whd in EX:(??%%); destruct
    921941      % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
    922942        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
    923         >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_state /2/ ]
     943        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
    924944      | skip ] | skip ]
    925945    ]
     
    943963    | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
    944964    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    945     ]| *: /2/ ]|*: skip]|*: skip ]
     965    ]| *: /3/ ]|*: skip]|*: skip ]
    946966  | #EX inversion KL
    947967    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    959979    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
    960980      [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
    961       | *: // ] | *: /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
     981      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
    962982    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    963983      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
     
    971991      | // | <(E0_right tr) @twel_app /2/
    972992      ]
    973       | /3/ | /2/ ] | *: skip ] | *: skip ]
     993      | /3/ | /3/ ] | *: skip ] | *: skip ]
    974994    ]
    975995  | * [2: #a ] #EX
     
    9941014      | >label_function_return >Ety in ⊢ (??%?);
    9951015      ] whd in ⊢ (??%?); @refl
    996       | *: // ]| *: @swl_returnstate /2/ ]|*:skip]|*:skip]
     1016      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
    9971017  | #a #ls #EX
    9981018    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    10131033    %[2: %[2: %[ %[ @plus_succ
    10141034      [ 4: @refl | 5: @plus_one @refl | *: skip ]
    1015       | /2/ ] | /2/ ] |skip ]| skip ]
     1035      | /2/ ] | /3/ ] |skip ]| skip ]
    10161036  | #l #EX
    10171037    whd in EX:(??%?);
     
    10251045      % [2: %[2: %[ %[ @plus_succ
    10261046        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
    1027         | /2/ ] | /2/ ] | skip ] | skip ]
     1047        | /2/ ] | /3/ ] | skip ] | skip ]
    10281048    ]
    10291049  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
    1030     % [2: % [2: % [ % [ @plus_one @refl | // ] | /2/ ] | skip ]| skip ]
     1050    % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
    10311051  ]
    10321052| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     
    10391059                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    10401060               |5: @plus_one @refl | *: skip ]
    1041     | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
     1061    | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
    10421062  | % [2: % [2: % [ % [
    10431063    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     
    10451065    | 5: @plus_succ [4: @refl
    10461066    | 5: @plus_one @refl | *: skip ] | *: skip ]
    1047     | <(E0_right tr) /3/ ]| /2/ ]| skip ]| skip ]
     1067    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
    10481068  ]
    10491069| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     
    10511071  % [2: % [2: % [ % [
    10521072    @plus_succ [4: % | 5: @plus_one % | *: skip ]
    1053     | /2/ ]| /3/ ]| skip ]| skip ]
     1073    | /2/ ]| /4/ ]| skip ]| skip ]
    10541074| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
    10551075  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    10611081                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    10621082    | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
    1063     | *: skip ]| <(E0_right tr) /3/ ] | /3/ ]| skip ]| skip ]
     1083    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
    10641084  | % [2: % [2: % [ % [
    10651085    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    10661086                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    10671087    | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
    1068     | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /2/ ]| skip ]| skip
    1069     ]
    1070   ]
    1071 | #f #u * [ #s | #sz #i #s #ls ] #k #k' #e #m #K #EX
    1072   whd in EX:(??(??(??%???))?);
     1088    | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
     1089    ]
     1090  ]
     1091| *
     1092  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
     1093    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
     1094    whd in EX:(??%%); destruct
     1095    whd in match (label_fundef ?);
     1096    whd in match (label_function ?);
     1097    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
     1098    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
     1099    % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
     1100      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
     1101    | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
     1102  | #id #tys #ty #args #k #k' #m #K #EX
     1103    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
     1104    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
     1105    whd in EX2:(??%%); destruct
     1106  ]
     1107| #res #k #k' #m #K #EX inversion K
     1108  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
     1109    [ 2: * #i #EX whd in EX:(??%?); destruct
     1110    | *: normalize #A try #B try #C destruct
     1111    ]
     1112    % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
     1113  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
     1114    [ #EX whd in EX:(??%?); destruct
     1115      % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
     1116    | * * #b #o #ty #EX
     1117      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
     1118      whd in EX:(??%%); destruct
     1119      % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
     1120    ]
     1121  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
     1122       destruct whd in EX:(??%?); destruct
     1123  ]
     1124| #r #EX whd in EX:(??%%); destruct
     1125] qed.
     1126
     1127lemma step_with_labels : ∀ge,ge'.
     1128  related_globals ge ge' →
     1129  ∀s1,s1',tr,s2.
     1130  state_with_labels s1 s1' →
     1131  (exec_step ge s1 = Value … 〈tr,s2〉 →
     1132   ∃tr',s2'. plus ge' s1' tr' s2' ∧
     1133             trace_with_extra_labels tr tr' ∧
     1134             state_with_labels s2 s2').
     1135#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
     1136[ #s1 #s1' @step_with_labels_partial //
     1137| #f #u *
     1138(* If we have LSdefault we need to smuggle the execution of the cost label in
     1139   before the actual statement. *)
     1140  [ #s #k #k' #e #m #K #EX
     1141    whd in EX:(??(??(??%???))?);
     1142    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
     1143    >shift_fst whd in match (seq_of_labeled_statement ?);
     1144    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
     1145    #tr' * #s2' * * #P #T #S
     1146    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
     1147(* but for LScase it's just like the cases in step_with_labels_partial *)
     1148  | #sz #i #s #ls #k #k' #e #m #K #EX
     1149    whd in EX:(??(??(??%???))?);
     1150    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
     1151    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
     1152    whd in EX:(??%?); destruct
     1153    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
     1154  ]   
     1155] qed.
     1156
     1157
     1158   
     1159
     1160
Note: See TracChangeset for help on using the changeset viewer.