Changeset 3448 for LTS/Language.ma


Ignore:
Timestamp:
Feb 19, 2014, 6:45:55 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3447 r3448  
    15491549        >memb_append_l1 // <(\P EQx_hdlab) >Hx // ]
    15501550    normalize nodelta >get_element_append_l1
    1551     [2: cases daemon (*noduplicates*)] @get_element_append_l1
     1551    [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail
     1552        [ whd in match (foldr ?????); @lab_map_in_domain // ]
     1553        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
     1554        >memb_append_l2 // >IH %
     1555    ] @get_element_append_l1
    15521556    % #H1 
    15531557    (* subproof with no nice statement *)
     
    15801584    ]
    15811585    ]
    1582   | whd #x #Hx >memb_append_l12 [2: cases daemon (*TODO*) ]
     1586  | whd #x #Hx >memb_append_l12
     1587    [2: @notb_Prop % #ABS @(memb_no_duplicates_append … H … Hx) elim tail
     1588        [ whd in match (foldr ?????); @lab_to_keep_in_domain // ]
     1589        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
     1590        >memb_append_l2 // >IH %
     1591    ]
    15831592    >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H)
    15841593    // @⊥
     
    16861695   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
    16871696   (((x ::l4 @y ::l3) @l8) @l9)).
     1697   
     1698lemma append_premeasurable : ∀S : abstract_status.
     1699∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
     1700pre_measurable_trace … t1 → pre_measurable_trace … t2 →
     1701pre_measurable_trace … (t1 @ t2).
     1702#S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre //
     1703[ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2
     1704  %2 // @IH //
     1705| #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH //
     1706| #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH //
     1707| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1
     1708  #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2
     1709  normalize >append_associative in ⊢ (????(???????%)); %5 // @IH2 //
     1710]
     1711qed.
    16881712   
    16891713
    1690 lemma correctness : ∀p,p',prog.
     1714lemma correctness_lemma : ∀p,p',prog.
    16911715no_duplicates_labels … prog →
    16921716let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     
    17001724                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
    17011725 len … t = len … t' ∧
    1702  ∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
     1726 (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
    17031727 cont … s1 = k @ cont … s2 →
    1704 All … (λx.let 〈lab,i〉 ≝ x in ¬ is_unlabelled_ret_act lab) k →
    1705 ∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|.
     1728∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|)
     1729∧ pre_measurable_trace … t'.
    17061730#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
    17071731#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
    17081732-abs_tail lapply s1' -s1' elim Hpre
    1709 [ #st #_ #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
     1733[ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
    17101734  %
    1711   [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
    1712     @is_permutation_eq
    1713   | #k #i #_ #EQcont_st #wf %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
    1714   ]
     1735  [ %
     1736    [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
     1737      @is_permutation_eq
     1738    | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
     1739    ]
     1740  | %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
     1741    #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize
     1742    inversion(code ??) normalize nodelta
     1743    [|#r_t| #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
     1744     | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #rlbl #i #_
     1745     | #lin #io #lout #i #_ ]
     1746    #EQcode_s1' normalize nodelta [|*: % #EQ destruct] <H2
     1747    >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     1748    normalize in Hst; <e1 in Hst; normalize nodelta //
     1749  ]   
    17151750| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    17161751  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
    1717     #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #_ * #opt_l #EQ destruct(EQ)
     1752    #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #class_st11 * #opt_l #EQ destruct(EQ)
    17181753    #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
    17191754    whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
     
    17391774      [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
    17401775           cases(call_post_clean ?????) normalize nodelta
    1741            [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
     1776           [1,3,5,7,9: #EQ destruct(EQ)]
     1777        [ * #z1 #z2 cases lbl normalize nodelta [|#z3 cases(?==?) normalize nodelta]
     1778          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1779        | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 ] whd in ⊢ (??%% → ?);
     1780          [2: cases(call_post_clean ?????) normalize nodelta
     1781          [| * #z5 #z6 cases(?∧?) normalize nodelta]] whd in ⊢ (??%% → ?);
     1782          #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1783        | * #z1 #z2 cases(call_post_clean ?????)
     1784          [| * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta]
     1785          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1786        | * #z1 #z2 cases ret_post normalize nodelta
     1787          [| #z3 cases(memb ???) normalize nodelta [ cases(?==?) normalize nodelta] ]
     1788          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1789        | * #z1 #z2 cases(?∧?) normalize nodelta
     1790          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1791        ]
     1792      ]
    17421793      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
    17431794      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
     
    17451796         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
    17461797         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1747       #abs_top' * #abs_tail' * #st3' * #t' *** #Hst3st3' #EQcosts #EQlen #stack_safety
     1798      #abs_top' * #abs_tail' * #st3' * #t' ****
     1799      #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t'
    17481800      %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
    17491801      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
    17501802        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1751       % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
     1803      %
     1804      [ % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
    17521805      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
    17531806      [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
    1754       destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     1807      destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
    17551808      #EQk1 #EQlength %{(〈cost_act (None ?),new_code'〉::k1)}
    1756       % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
     1809      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]
     1810      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11
     1811      normalize in class_st11; >EQcode11 in class_st11; //
    17571812    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
    17581813      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
     
    17661821      | #l_in #io #l_out #i #_
    17671822      ]
    1768       [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
     1823      [|*: #_ whd in ⊢ (??%% → ?);
     1824           [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1825           | cases(call_post_clean ?????) normalize nodelta
     1826             [| * #z2 #z3 cases lbl normalize nodelta
     1827                [| #z4 cases(?==?) normalize nodelta] ]
     1828             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1829           | cases(call_post_clean ?????) normalize nodelta
     1830             [| * #z2 #z3 cases(call_post_clean ?????)
     1831               [| * #z4 #z5 >m_return_bind cases(call_post_clean ?????)
     1832                  [| * #z6 #z7 >m_return_bind cases(?∧?) normalize nodelta ]]]
     1833             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1834           |  cases(call_post_clean ?????) normalize nodelta
     1835             [| * #z2 #z3 cases(call_post_clean ?????)
     1836                [| * #z4 #z5 >m_return_bind cases(?∧?) normalize nodelta ]]
     1837             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1838           | cases(call_post_clean ?????) normalize nodelta
     1839             [| * #z1 #z2 cases ret_post normalize nodelta
     1840                [| #z3 cases(memb ???) normalize nodelta
     1841                   [ cases (?==?) normalize nodelta]]]
     1842             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1843           | cases(call_post_clean ?????) normalize nodelta
     1844             [| * #z1 #z2 cases(?∧?) normalize nodelta ]
     1845             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1846           ]
     1847      ]
    17691848      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
    17701849      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
     
    17731852         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
    17741853         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1775       #abs_top' * #abs_tail' * #st3' * #t' *** #Hst3st3' #EQcost #EQlen #stack_safety
     1854      #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcost #EQlen #stack_safety
     1855      #pre_t'
    17761856      %{abs_top'} %{abs_tail'} %{st3'}
    17771857      %{(t_ind … (cost_act (Some ? lbl)) … t')}
    17781858      [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
    17791859        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1780       % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
     1860      %
     1861      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
    17811862          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
    17821863          @is_permutation_cons assumption
    17831864        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
    17841865          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
    1785           destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     1866          destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
    17861867          #EQk1 #EQlength %{(〈cost_act (Some ? lbl),new_code'〉::k1)}
    17871868          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    1788         ]
     1869        ]]
     1870      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio
     1871      normalize in class_st11; >EQcode11 in class_st11; //
    17891872    ]
    17901873  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
     
    17941877    ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
    17951878    #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ]
    1796     inversion(code ??) [1,2,4,5,6,7,8,9,11,12,13,14: cases daemon (*assurdi*)]
     1879    inversion(code ??)
     1880    [1,2,4,5,6,7,8,9,11,12,13,14:
     1881      [1,7: #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1882      |2,8: #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1883      |3,9: #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     1884            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1885            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     1886                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     1887                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     1888            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1889      |4,10:  #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     1890            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1891            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     1892                [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     1893            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1894      |5,11: #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1895             normalize nodelta
     1896             [2,4: * #z1 #z2 cases lbl normalize nodelta
     1897               [2,4: #l1 cases(memb ???) normalize nodelta
     1898                 [1,3: cases(?==?) normalize nodelta ]]]
     1899            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1900      |6,12: #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1901             normalize nodelta
     1902             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     1903             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1904      ]
     1905    ]
    17971906    #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?);
    17981907    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
     
    18101919    |2,5:
    18111920    ]
    1812     #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1813     %{abs_top1}
     1921    #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1922    #pre_t' %{abs_top1}
    18141923    %{abs_tail1} %{s2'} %{(t_ind … t')}
    18151924    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
    18161925    |2,5:
    18171926    ]
    1818     % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
     1927    % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
    18191928        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
    18201929        whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
    18211930        assumption
    1822       |*: #k #i #EQcont_st3 >EQcont #EQ #H
    1823           cases(stack_safety … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
    1824       ]
     1931      |*: #k #i #EQcont_st3 >EQcont #EQ
     1932          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
     1933      ]]
     1934    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    18251935  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    18261936    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    18281938    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
    18291939    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1830     [1,2,3,5,6,7: cases daemon (*ASSURDI*)] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
     1940    [1,2,3,5,6,7:
     1941     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1942     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1943     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1944       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     1945       [2: #l1 cases(?==?) normalize nodelta]]
     1946       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1947     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     1948       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1949       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     1950       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     1951       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1952     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1953             normalize nodelta
     1954             [2,4: * #z1 #z2 cases lbl normalize nodelta
     1955               [2,4: #l1 cases(memb ???) normalize nodelta
     1956                 [1,3: cases(?==?) normalize nodelta ]]]
     1957            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1958     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     1959             normalize nodelta
     1960             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     1961             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1962      ]
     1963    ]
     1964    #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
    18311965    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    18321966    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
     
    18451979        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    18461980        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1847     ] #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcost #EQlen
    1848       #stack_safety %{abs_top1} %{abs_tail1}
     1981    ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
     1982      #stack_safety #pre_t' %{abs_top1} %{abs_tail1}
    18491983    %{s2'} %{(t_ind … t')}
    18501984    [ @hide_prf @(cond_true … EQcode_s1') //
    18511985    |
    18521986    ]
    1853     %
     1987    % [ %
    18541988    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    18551989      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    18561990      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
    18571991      assumption
    1858     |  #k #i1 #EQcont_st3 #EQcont_st11 #H
     1992    |  #k #i1 #EQcont_st3 #EQcont_st11
    18591993       cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
    1860        [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     1994       [2: >EQcont_st12 >EQcont_st11 % ]
    18611995       * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    18621996       %{tl1} % // whd in EQk1 : (??%%); destruct //
    1863     ]
     1997    ]]
     1998    %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    18641999  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    18652000    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
     
    18672002    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
    18682003    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1869     [1,2,3,5,6,7: cases daemon (*ASSURDI*)] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
     2004    [1,2,3,5,6,7:
     2005     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2006     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2007     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2008       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2009       [2: #l1 cases(?==?) normalize nodelta]]
     2010       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2011     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2012       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2013       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2014       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2015       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2016     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2017             normalize nodelta
     2018             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2019               [2,4: #l1 cases(memb ???) normalize nodelta
     2020                 [1,3: cases(?==?) normalize nodelta ]]]
     2021            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2022     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2023             normalize nodelta
     2024             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2025             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2026      ]
     2027    ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
    18702028    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    18712029    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
     
    18842042        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    18852043        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1886     ] #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcost #EQlen #stack_safety
     2044    ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
     2045    #pre_t'
    18872046    %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    18882047    [ @hide_prf @(cond_false … EQcode_s1') //
    18892048    |
    18902049    ]
    1891     %
     2050    % [ %
    18922051    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    18932052      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    18942053      >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
    18952054      assumption
    1896     | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2055    | #k #i1 #EQcont_st3 #EQcont_st11
    18972056      cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
    1898       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2057      [2: >EQcont_st12 >EQcont_st11 % ]
    18992058      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    19002059      %{tl1} % // whd in EQk1 : (??%%); destruct //
    1901     ]
     2060    ] ]
     2061    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19022062 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
    19032063   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
    19042064   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
    19052065   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1906    [1,2,3,4,6,7: cases daemon (*assurdi*) ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
     2066   [1,2,3,4,6,7:
     2067     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2068     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2069     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2070       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2071       [2: #l1 cases(?==?) normalize nodelta]]
     2072       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2073     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2074            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2075            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2076                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2077                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2078            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2079     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2080             normalize nodelta
     2081             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2082               [2,4: #l1 cases(memb ???) normalize nodelta
     2083                 [1,3: cases(?==?) normalize nodelta ]]]
     2084            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2085     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2086             normalize nodelta
     2087             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2088             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2089      ]
     2090   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
    19072091   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    19082092   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
     
    19232107       % //
    19242108   ]
    1925    #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1926    %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2109   #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2110   #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19272111   [ @hide_prf @(loop_true … EQcode_s1') // |]
    1928    %
     2112   % [ %
    19292113   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    19302114     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    19312115      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    19322116     @is_permutation_cons assumption
    1933    | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2117   | #k #i1 #EQcont_st3 #EQcont_st11
    19342118      cases(stack_safety … (〈cost_act (None NonFunctionalLabel), LOOP p cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …)
    1935       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2119      [2: >EQcont_st12 >EQcont_st11 % ]
    19362120      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    19372121      %{tl1} % // whd in EQk1 : (??%%); destruct //
    1938    ]
     2122   ] ]
     2123   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19392124 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
    19402125   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
    19412126   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
    19422127   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1943    [1,2,3,4,6,7: cases daemon (*assurdi*) ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
     2128   [1,2,3,4,6,7:
     2129     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2130     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2131     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2132       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2133       [2: #l1 cases(?==?) normalize nodelta]]
     2134       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2135     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2136            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2137            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2138                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2139                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2140            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2141     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2142             normalize nodelta
     2143             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2144               [2,4: #l1 cases(memb ???) normalize nodelta
     2145                 [1,3: cases(?==?) normalize nodelta ]]]
     2146            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2147     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2148             normalize nodelta
     2149             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2150             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2151      ]
     2152   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
    19442153   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    19452154   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
     
    19582167        % // % // % // % [2: %] //
    19592168   ]
    1960    #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1961    %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2169   #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2170   #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19622171   [ @hide_prf @(loop_false … EQcode_s1') // |]
    1963    %
     2172   % [ %
    19642173   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    19652174     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    19662175     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    19672176     @is_permutation_cons assumption
    1968    | #k #i #EQcont_st3 <EQcont_st12 #EQ #H
    1969      cases(stack_safety … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
    1970    ]
     2177   | #k #i #EQcont_st3 <EQcont_st12 #EQ
     2178     cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
     2179   ]]
     2180   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    19712181 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
    19722182   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
     
    19742184   [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
    19752185   #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
    1976    [1,2,3,4,5,6: cases daemon (*ASSURDI*)] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
     2186   [1,2,3,4,5,6:
     2187     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2188     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2189     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2190       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2191       [2: #l1 cases(?==?) normalize nodelta]]
     2192       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2193     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2194            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2195            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2196                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2197                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2198            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2199     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2200       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2201       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2202       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2203       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2204     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2205             normalize nodelta
     2206             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2207               [2,4: #l1 cases(memb ???) normalize nodelta
     2208                 [1,3: cases(?==?) normalize nodelta ]]]
     2209            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2210      ]
     2211   ] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
    19772212   whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
    19782213   [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta
     
    19892224       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    19902225   ]
    1991    #abs_cont1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1992    %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2226   #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2227   #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    19932228   [ @hide_prf @(io_in … EQcode_s1') // |]
    1994    %
     2229   % [ %
    19952230   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
    19962231     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
    19972232     >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    19982233     @is_permutation_cons assumption
    1999    | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2234   | #k #i1 #EQcont_st3 #EQcont_st11
    20002235      cases(stack_safety … (〈cost_act (Some ? lout),i〉::k) … EQcont_st3 …)
    2001       [2: >EQcont_st12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2236      [2: >EQcont_st12 >EQcont_st11 %]
    20022237      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    20032238      %{tl1} % // whd in EQk1 : (??%%); destruct //
    2004    ]
     2239   ]]
     2240   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    20052241  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    20062242    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
     
    20082244    destruct #t #_ * #nf #EQ destruct
    20092245  ]
    2010 | #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?; [1,2,3,4,5,6,7,8: cases daemon (*assurdi*)]
     2246| #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?;
     2247  [1,2,3,4,5,6,7,8:
     2248    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
     2249    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
     2250    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
     2251    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
     2252    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2253    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2254    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
     2255    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
     2256    ]
     2257    destruct #tl * #y #EQ destruct(EQ) @⊥ >EQ in x12; * #ABS @ABS %
     2258  ]
    20112259  #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ)
    20122260  #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6)
     
    20282276  inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    20292277  ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?);
    2030   inversion(code … s1') [1,3,4,5,6,7: cases daemon (*TODO*) ] #r_t' #EQcode_s1'
     2278  inversion(code … s1')
     2279  [1,3,4,5,6,7:
     2280     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2281     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2282       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2283       [2: #l1 cases(?==?) normalize nodelta]]
     2284       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2285     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2286            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2287            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2288                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2289                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2290            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2291     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2292       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2293       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2294       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2295       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2296     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2297             normalize nodelta
     2298             [2,4: * #z1 #z2 cases lbl normalize nodelta
     2299               [2,4: #l1 cases(memb ???) normalize nodelta
     2300                 [1,3: cases(?==?) normalize nodelta ]]]
     2301            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2302     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2303             normalize nodelta
     2304             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2305             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2306      ]
     2307  ]
     2308   #r_t' #EQcode_s1'
    20312309  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    20322310  #EQstore11 #EQio_11 #EQ destruct
    20332311  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    20342312  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    2035   #abs_top1 * #abs_tail1 * #s2' * #t' *** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2036   %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2313  #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2314  #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
    20372315  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    20382316  | ]
    2039   %
     2317  % [ %
    20402318  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
    20412319    whd in match (get_costlabels_of_trace ????);
     
    20452323  | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%);
    20462324    [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
    2047     destruct * #_ #H cases(stack_safety … EQcont_st3 … e0 H) #k1 *
     2325    destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
    20482326    #EQk1 #EQlength %{(〈ret_act (Some ? lbl1),i〉::k1)}
    20492327    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    2050   ]
     2328  ]]
     2329  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    20512330| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
    2052   [1,2,3,4,5,6,7,9: cases daemon (*absurd!*)
     2331  [1,2,3,4,5,6,7,9:
     2332    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
     2333    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
     2334    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
     2335    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
     2336    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2337    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
     2338    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
     2339    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
     2340    ]
     2341    destruct * #z1 * #z2 #EQ destruct(EQ) whd in ⊢ (?% → ?); >x3 in ⊢ (% → ?); *
    20532342  | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
    20542343    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
     
    20592348    #abs_top_cont #abs_tail_cont #EQcheck
    20602349    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
    2061     [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
     2350    [1,2,3,4,5,7:
     2351     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2352     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2353     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2354       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
     2355       [2: #l1 cases(?==?) normalize nodelta]]
     2356       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2357     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
     2358            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2359            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2360                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
     2361                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
     2362            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2363     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
     2364       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2365       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
     2366       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
     2367       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2368     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
     2369             normalize nodelta
     2370             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
     2371             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     2372     ]
     2373    ] #f' #act_p' #opt_l' #i' #_
    20622374    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
    20632375    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
     
    20922404            ]
    20932405          ]
    2094           #abs_top''' * #abs_tail''' * #st3' * #t' *** #Hst3st3' #EQcosts #EQlen #stack_safety
    2095           %{abs_top'''}
     2406          #abs_top''' * #abs_tail''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
     2407          #pre_t' %{abs_top'''}
    20962408          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    20972409          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
    2098           %
     2410          % [ %
    20992411          [ % [2: whd in ⊢ (??%%); >EQlen %]
    21002412            %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     
    21032415            whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
    21042416            >append_nil whd in match (append ???) in ⊢ (???%); //
    2105           | #k #i1 #EQcont_st3 #EQcont_st11 #H
     2417          | #k #i1 #EQcont_st3 #EQcont_st11
    21062418            cases(stack_safety … (〈ret_act (Some ? lbl),i〉::k) … EQcont_st3 …)
    2107             [2: >EQcont12 >EQcont_st11 % |3: % // % whd in ⊢ (% → ?); #EQ destruct]
     2419            [2: >EQcont12 >EQcont_st11 % ]
    21082420            * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
    21092421            %{tl1} % // whd in EQk1 : (??%%); destruct //
    2110           ]
     2422          ]]
     2423          %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
    21112424        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
    21122425        ]
     
    21642477          ]
    21652478     ]
    2166      #abs_top''' * #abs_tail''' * #st41' * #t1' *** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2479     #abs_top''' * #abs_tail''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2480     #pre_t1'
    21672481     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
    21682482     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
     
    21932507             abs_tail_cont abs_top'''')
    21942508     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2195      #abs_top_1 * #abs_tail_1 * #st5' * #t2' *** #Hst5_st5' #EQcosts'
    2196      #EQlen'  #stack_safety2 %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     2509     #abs_top_1 * #abs_tail_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
     2510     #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
    21972511     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    21982512     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
    21992513     |2,4: skip
    22002514     ]
    2201      %
     2515     % [ %
    22022516     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
    22032517           whd in ⊢ (??%%); @eq_f // ]
     
    22142528       cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
    22152529       >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
    2216      | #k #i #EQcont_st3 #EQ #H
    2217        cases(stack_safety2 … EQcont_st3 … EQ H) #k1 * #EQk1 #EQlength %{k1} % //
     2530     | #k #i #EQcont_st3 #EQ
     2531       cases(stack_safety2 … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
     2532     ]]
     2533     %4
     2534     [ normalize >EQcode_st1' normalize nodelta % #EQ destruct
     2535     | %{f} % //
     2536     | whd in ⊢ (?%); >EQcode_st1' normalize nodelta @I
     2537     | @append_premeasurable // %3 //
     2538       [ whd in match (as_classify ??); >EQcode_st41' normalize nodelta % #EQ destruct
     2539       | whd %{lbl'} %
     2540       ]
    22182541     ]
    22192542]
Note: See TracChangeset for help on using the changeset viewer.