equal
deleted
inserted
replaced
21 |
21 |
22 map_emp :: i |
22 map_emp :: i |
23 "map_emp == 0" |
23 "map_emp == 0" |
24 |
24 |
25 map_owr :: "[i,i,i]=>i" |
25 map_owr :: "[i,i,i]=>i" |
26 "map_owr(m,a,b) == \<Sigma>x \<in> {a} Un domain(m). if x=a then b else m``{x}" |
26 "map_owr(m,a,b) == \<Sigma> x \<in> {a} Un domain(m). if x=a then b else m``{x}" |
27 |
27 |
28 map_app :: "[i,i]=>i" |
28 map_app :: "[i,i]=>i" |
29 "map_app(m,a) == m``{a}" |
29 "map_app(m,a) == m``{a}" |
30 |
30 |
31 lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})" |
31 lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})" |