729 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
729 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
730 p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
730 p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p" |
731 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
731 "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow> |
732 p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
732 p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p" |
733 using point.simps bw_point.simps |
733 using point.simps bw_point.simps |
734 by smt+ (* FIXME: bad Z3-4.3.x proof with smt2 *) |
734 by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *) |
735 |
735 |
736 lemma |
736 lemma |
737 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
737 "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>" |
738 "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
738 "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> = |
739 \<lparr> cx = 3, cy = 4, black = False \<rparr>" |
739 \<lparr> cx = 3, cy = 4, black = False \<rparr>" |