#Processed by Id: cwm.py,v 1.59 2001/07/03 16:55:52 connolly Exp # using base file:/n3/ # Notation3 generation by # notation3.py,v 1.83 2001/06/25 06:35:50 connolly Exp # Base was: file:/n3/ @prefix : . @prefix log: . this log:forSome <#_gs44>, <#_gs4>, . [ :apoint [ :X :3; :Y :6 ]; :center [ :X :0; :Y :2 ]; :radius ; :tpoint [ :X [ :product [ :sum [ :product [ :square <#_gs44> ], :3 ], [ :minus [ :product <#_gs44>, :6 ] ], :0, [ :product <#_gs44>, :2 ] ], [ :slash [ :sum [ :square <#_gs44> ], :1 ] ] ]; :Y [ :product [ :sum [ :product <#_gs44>, :0 ], [ :product [ :square <#_gs44> ], :2 ], [ :minus [ :product <#_gs44>, :3 ] ], :6 ], [ :slash [ :sum [ :square <#_gs44> ], :1 ] ] ] ] ]. [ :apoint [ :X :3; :Y :6 ]; :center [ :X :0; :Y :2 ]; :radius ; :slope <#_gs4> ]. [ :apoint [ :X :3; :Y :6 ]; :center [ :X :0; :Y :2 ]; :radius ; :slope <#_gs44> ]. <#_gs44> :product [ :sum [ :minus [ :product :2, :3, [ :sum :6, [ :minus :2 ] ] ] ], [ :minus [ :sqrt [ :sum [ :product :4, [ :square :3 ], [ :square [ :sum :6, [ :minus :2 ] ] ] ], [ :minus [ :product :4, [ :sum [ :square ], [ :minus [ :square [ :sum :0, [ :minus :3 ] ] ] ] ], [ :sum [ :square ], [ :minus [ :square [ :sum :2, :6 ] ] ], [ :product :2, [ :sum :0, [ :minus :6 ] ] ] ] ] ] ] ] ] ], [ :slash [ :product :2, [ :sum [ :square ], [ :minus [ :square [ :sum :0, [ :minus :3 ] ] ] ] ] ] ] . <#_gs4> :product [ :slash [ :product :2, [ :sum [ :square ], [ :minus [ :square [ :sum :0, [ :minus :3 ] ] ] ] ] ] ], [ :sum [ :minus [ :product :2, :3, [ :sum :6, [ :minus :2 ] ] ] ], [ :sqrt [ :sum [ :product :4, [ :square :3 ], [ :square [ :sum :6, [ :minus :2 ] ] ] ], [ :minus [ :product :4, [ :sum [ :square ], [ :minus [ :square [ :sum :0, [ :minus :3 ] ] ] ] ], [ :sum [ :square ], [ :minus [ :square [ :sum :2, :6 ] ] ], [ :product :2, [ :sum :0, [ :minus :6 ] ] ] ] ] ] ] ] ] . [ :apoint [ :X :3; :Y :6 ]; :center [ :X :0; :Y :2 ]; :radius ; :tpoint [ :X [ :product [ :sum [ :product [ :square <#_gs4> ], :3 ], [ :minus [ :product <#_gs4>, :6 ] ], :0, [ :product <#_gs4>, :2 ] ], [ :slash [ :sum [ :square <#_gs4> ], :1 ] ] ]; :Y [ :product [ :sum [ :product <#_gs4>, :0 ], [ :product [ :square <#_gs4> ], :2 ], [ :minus [ :product <#_gs4>, :3 ] ], :6 ], [ :slash [ :sum [ :square <#_gs4> ], :1 ] ] ] ] ]. [ :apoint [ :X :3; :Y :6 ]; :center [ :X :0; :Y :2 ]; :radius ]. :product [ :slash [ :sqrt :5 ] ], :2 . { { [ :apoint [ :X :x1; :Y :y1 ]; :center [ :X :x0; :Y :y0 ]; :radius :r ]. } log:implies { [ :apoint [ :X :x1; :Y :y1 ]; :center [ :X :x0; :Y :y0 ]; :radius :r; :slope [ :product [ :sum [ :minus [ :product :2, :x1, [ :sum :y1, [ :minus :y0 ] ] ] ], [ :sqrt [ :sum [ :product :4, [ :square :x1 ], [ :square [ :sum :y1, [ :minus :y0 ] ] ] ], [ :minus [ :product :4, [ :sum [ :square :r ], [ :minus [ :square [ :sum :x0, [ :minus :x1 ] ] ] ] ], [ :sum [ :square :r ], [ :minus [ :square [ :sum :y0, :y1 ] ] ], [ :product :2, :y0, [ :sum :x0, [ :minus :y1 ] ] ] ] ] ] ] ] ], [ :slash [ :product :2, [ :sum [ :square :r ], [ :minus [ :square [ :sum :x0, [ :minus :x1 ] ] ] ] ] ] ] ] ]. } . } a log:Truth; log:forAll :r, :x0, :x1, :y0, :y1 . { { [ :apoint [ :X :x1; :Y :y1 ]; :center [ :X :x0; :Y :y0 ]; :radius :r ]. } log:implies { [ :apoint [ :X :x1; :Y :y1 ]; :center [ :X :x0; :Y :y0 ]; :radius :r; :slope [ :product [ :sum [ :minus [ :product :2, :x1, [ :sum :y1, [ :minus :y0 ] ] ] ], [ :minus [ :sqrt [ :sum [ :product :4, [ :square :x1 ], [ :square [ :sum :y1, [ :minus :y0 ] ] ] ], [ :minus [ :product :4, [ :sum [ :square :r ], [ :minus [ :square [ :sum :x0, [ :minus :x1 ] ] ] ] ], [ :sum [ :square :r ], [ :minus [ :square [ :sum :y0, :y1 ] ] ], [ :product :2, :y0, [ :sum :x0, [ :minus :y1 ] ] ] ] ] ] ] ] ] ], [ :slash [ :product :2, [ :sum [ :square :r ], [ :minus [ :square [ :sum :x0, [ :minus :x1 ] ] ] ] ] ] ] ] ]. } . } a log:Truth; log:forAll :r, :x0, :x1, :y0, :y1 . { { [ :apoint [ :X :x1; :Y :y1 ]; :center [ :X :x0; :Y :y0 ]; :radius :r; :slope :m ]. } log:implies { [ :apoint [ :X :x1; :Y :y1 ]; :center [ :X :x0; :Y :y0 ]; :radius :r; :tpoint [ :X [ :product [ :sum [ :product [ :square :m ], :x1 ], [ :minus [ :product :m, :y1 ] ], :x0, [ :product :m, :y0 ] ], [ :slash [ :sum [ :square :m ], :1 ] ] ]; :Y [ :product [ :sum [ :product :m, :x0 ], [ :product [ :square :m ], :y0 ], [ :minus [ :product :m, :x1 ] ], :y1 ], [ :slash [ :sum [ :square :m ], :1 ] ] ] ] ]. } . } a log:Truth; log:forAll :m, :r, :x0, :x1, :y0, :y1 . #ENDS