24 value "count_list (2::nat) [2,2,1]"

    24 value "count_list (2::nat) [2,2,1]"

    25 

    25 

    26 lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys"

    26 lemma count1: "count_list n(xs @ ys) = count_list n xs + count_list n ys"

    27 apply(induct xs)

    27 apply(induct xs)

    28 apply(auto)

    28 apply(auto)

    29  

    30  

    30  

    31  

    31 

    32 

    32 

    33 

    33 

    34