64 lemma "[a, b, c] @ xs = a # b # c # xs" by normalization |
64 lemma "[a, b, c] @ xs = a # b # c # xs" by normalization |
65 lemma "[] @ xs = xs" by normalization |
65 lemma "[] @ xs = xs" by normalization |
66 lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization |
66 lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization |
67 |
67 |
68 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" |
68 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" |
69 by normalization |
69 by normalization rule |
70 lemma "rev [a, b, c] = [c, b, a]" by normalization |
70 lemma "rev [a, b, c] = [c, b, a]" by normalization |
71 value [nbe] "rev (a#b#cs) = rev cs @ [b, a]" |
71 value [nbe] "rev (a#b#cs) = rev cs @ [b, a]" |
72 value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])" |
72 value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])" |
73 value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" |
73 value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" |
74 value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" |
74 value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" |