1. POSITION::=Net{ x,y:Nat0 },
2. pixels::=$ POSITION. To make this treatment simpler, assume that we can work with a logical window that is unlimitted and delay tackling problems of graphics leaving the physical screen or display. There exist well techniques for doing this any way.

3. For p: pixels, neighbours(p)::@pixels={n:pixels || p.x-1<=n.x<=p.x+1 and p.y-1<=n.y<=p.y+1}.

4. For p,q: pixels, p next_to q::@=q in neighbours(p).
   
5. (above)|- (g0): next_to in Reflexive(pixels) & Symmetric(pixels)~transitive(pixels).

   Proof of g0

   Reflexive and Symmetric follow by substitution of definitions and rearrangement. Lack of transitivity comes form considering pixels (0,1),(0,2),(0,3).

6. For S:@pixels,
7. outside(S)::@pixels=pixels~S,
8. close(S)::@pixels= |neighbours(S),
9. inside(S)::@pixels= outside(close(outside(S))),
10. edge(S)::@pixels=close(S)~inside(S).

11. colors::={white, black, ...}.

12. pictures::=pixels->colors

    For o:{+,-, div, mod, *, /}, o::infix(pixels) = (x=>(1st).x o (2nd).x, y=>(1st).y o (2nd).y).
    

13. (above)|- (g1): For a,b:pixels, o:{+,-, div, mod, *, /}, a o b = (x=>a.x o b.x, y=>a.y o b.y).
14. For a:pixels, n:Real, n * a::pixels= (x=> round(n * a.x), y=> round(n * a.y) ).

    
    

15. (above)|- (g2): MODULE(M=>pixels, Ring=>Reals).

16. WIDTH_DEPTH::=Net{ w, d:Numbers&positive, width:=w, depth:=d. wd:=(x=>w,y=>d)}.

17. PATTERN::=
    Net{

    WIDTH_DEPTH.
    1. basis::$ POSITION and {0<=x<=w, 0<=y<=d} ->colors.
    2. cycle::=(x=>w+1, y=>d+1).

    3. color::points->colors=map[p:points](basis(p mod cycle))

    
    }=::PATTERN.

18. pattern::={none} \/ $ PATTERN.

19. RECTANGLE::=
    Net{

    WIDTH_DEPTH. tl, tr, br, bl, c::pixels,
    1. top_left::=tl, top_right::=tr, bottom_right::=br,bottom_left::=tr,
    2. center::=centre::=c.

    3. br=tl+wd.
    4. c = tl + 0.5*wd.
    5. l::=left::=tl.x, l=bl.x, r::=right::=tr.x, r=br.x,
    6. t::=top:=tl.y, t=tr.y, b::=bottom::=bl.y, b=br.y.

    7. coverage::={p:pixels || tl.x<=p.x<=tr.x and tl.y<=p.y<=br.y}

    
    }=::RECTANGLE.

20. GRAPHIC::=
    Net{

    1. coverage::@pixels, - part filled with pattern
    2. contacts::@coverage, - pixels where it can touch another graphic.
    3. shape::Sets, fill, pen::pattern,
    4. type::{line,box,...}.
    5. (gt1): type=line iff LINE.
    6. (gt2): type = box iff BOX.

       [click here if you can fill this hole]

    
    }=::GRAPHIC.

21. graphics::@$ GRAPHIC.

22. THIN::=Net{ GRAPHIC. inside={}}.

23. LINE::=
    Net{

    start, end::pixels.
    
    1. |- (gl0): GRAPHIC and Net{type=line}.
       
    2. |- (gl1): contacts={start, end}.
       
    3. |- (gl2): for all p,q in coverage. p do(next_to) q.
       
    4. |- (gl3): shape={horizontal, vertical, straight, curved,...}.
       
    5. |- (gl4): pen=fill.
    6. arrow_heads::@{start,finish,middle}><{open,closed}><{hollow, thin, thick,...}.

    
    }=::LINE.

24. BOX::=
    Net{

    RECTANGLE. Assume that there are no holes or projections.
    1. Boxes are supposed to cover a rectangular area.
       
    2. |- (gb0): GRAPHIC and Net{type=box}.

       
       

    3. |- (gb1): contacts=edge(coverage).
       
    4. |- (gb2): shape={rectangle, text, char, blob}.

    
    }=::BOX.

25. touches::Reflexive(graphics).

    
    

26. |- (g4): PART_WHOLE(graphics, is_part_of).

    
    

27. |- (g5): for all g1,g2:graphics, if g1 touches g2 then not g1 is_part_of g2.
    
28. |- (g6): for all g1,g2:graphics, if g1 is_part_of g2 then coverage(g1)==>coverage(g2)).

    |-(g7): for all g1,g2:graphics, g1 overlaps g2::@ =some coverage(g1)& coverage(g2)).

    
    

29. |- (g8): for all g1,g2:graphics, if not g1 (is_part_of | /is_part_of) g2 then not g1 overlaps g2 ).

    
    

30. |- (g9): for all g1,g2:graphics, if g1 touches g2 then some close contacts(g1) & close contacts(g2).

31. above::@(qraphics,graphics)=rel[a,b](b.l<=a.l and a.r<=b.r and a.c.y>b.c.y),
32. below::@(qraphics,graphics)= /above.
33. left::@(graphics,graphics)=rel[a,b](a.t<=b.t and a.b>=b.b and a.c.x<b.c.x),
34. right::@(qraphics,graphics)= /left.

    [ logic_8_Natural_Language.html ]

. . . . . . . . . ( end of section Simple Graphics) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see