(************** Content-type: application/mathematica **************
CreatedBy='Mathematica 4.2'
Mathematica-Compatible Notebook
This notebook can be used with any Mathematica-compatible
application, such as Mathematica, MathReader or Publicon. The data
for the notebook starts with the line containing stars above.
To get the notebook into a Mathematica-compatible application, do
one of the following:
* Save the data starting with the line of stars above into a file
with a name ending in .nb, then open the file inside the
application;
* Copy the data starting with the line of stars above to the
clipboard, then use the Paste menu command inside the application.
Data for notebooks contains only printable 7-bit ASCII and can be
sent directly in email or through ftp in text mode. Newlines can be
CR, LF or CRLF (Unix, Macintosh or MS-DOS style).
NOTE: If you modify the data for this notebook not in a Mathematica-
compatible application, you must delete the line below containing
the word CacheID, otherwise Mathematica-compatible applications may
try to use invalid cache data.
For more information on notebooks and Mathematica-compatible
applications, contact Wolfram Research:
web: http://www.wolfram.com
email: info@wolfram.com
phone: +1-217-398-0700 (U.S.)
Notebook reader applications are available free of charge from
Wolfram Research.
*******************************************************************)
(*CacheID: 232*)
(*NotebookFileLineBreakTest
NotebookFileLineBreakTest*)
(*NotebookOptionsPosition[ 1737459, 49180]*)
(*NotebookOutlinePosition[ 1839999, 51908]*)
(* CellTagsIndexPosition[ 1831699, 51721]*)
(*WindowFrame->Normal*)
Notebook[{
Cell[CellGroupData[{
Cell["TH\[Exists]OREM\[ForAll]", "Subtitle",
TextAlignment->Center,
TextJustification->0,
FontSize->36],
Cell[TextData[StyleBox["Bruno Buchberger\n\nRISC and RICAM\nLinz, Austria\n\
Bruno.Buchberger@RISC.Uni-Linz.ac.at",
FontSlant->"Plain"]], "Subsubtitle",
TextAlignment->Center,
TextJustification->0,
CellTags->"Built\[Dash]in (PauleSchorn)"],
Cell[TextData[{
StyleBox["Copyright Bruno Buchberger 2004.",
FontWeight->"Bold"],
"\n\n",
StyleBox["Copyright Note: ",
FontWeight->"Bold"],
"This file can be copied and stored under the following conditions:\n\n- \
the file must be kept unchanged including the copyright note\n- an note must \
be sent to buchberger@risc.uni-linz.ac.at\n- the talk should be cited \
appropriately if material from this talk is used."
}], "Text"],
Cell[TextData[{
StyleBox["Acknowledgement to ",
FontWeight->"Bold"],
StyleBox["Theorema",
FontWeight->"Bold",
FontSlant->"Italic"],
StyleBox[" Group: \n",
FontWeight->"Bold"],
"\nT. Jebelean, T. Kutsia, (K. Nakagawa), M. Rosenkranz, W. Windsteiger.\n\n\
A. Craciun, F. Piroi. "
}], "Text"],
Cell[CellGroupData[{
Cell["The Goal of Theorema", "Section"],
Cell[CellGroupData[{
Cell["Support Mathematical Theory Exploration", "Subsubsection"],
Cell[GraphicsData["Metafile", "\<\
CF5dJ6E]HGAYHf4PEfU^I6mgLb15CDHPAVmbKF5d0@0000l`0@0006`0000:0000o_ooofL2000J0P00
00000000001_>`00acH00215CDH00040<0l0070000030000000000000000000000@00003003n0000
b`000000000000000000033P0`3h60<02P000100000`0000<`0000T0000@0000H`800182000D0000
300000d000160000:00001`00017A4U30P000;d0000b0000T`8004@200000000G`0003P000010000
>0000000000h0000000000020@090000000009W<0000000000000000000U000030000040000U0000
300000D0080k0000200001/0000@0000>P4005L1001H0000n080000000000000oooooooooong0000
?`540DL1<@5A0Al1E@4F0Ed11@5T0Oh0I`7k07H1lP1k0Nl0Q07Y08P1h@2C0M`0Y`7D0;X1cP3@0LT0
0@;?0382e`1S0]`0I0;O06H2h`1W0^H0J@;Y06/2k01]0^l0M@810G/26P690RP1T@9?0HX2M05o0YX1
OP:V0Gh2/`5k0[l1N`;20GL2`P5f0/@1K`;>0GL2c@5X0]81G@;F0E82f@570]`1A0;P0D42iP4m0^T1
>`;/0CL2k@4d0^l1<0;b0Bh2m`4Z0_P160800PT22`;k0AT2nP4N0_/190;g0BP2l`4[0^d1:P;X0B`2
``4h0_@1:P;<0CD2[0570XH1>P9T0CH2G@4e0TH1<08n0Bd2=P4Z0RL1908W0B@2704=0Qh1408:0@L2
1`440PD100810Oh1o@3l0OD0n07b0?@1j`3^0Ml0h@7O0>41gP3N0Md0f`7K0=P1f03D0M<0d`7A0
l0fP3V0=d0f`3S0=<0i03A0>L0d03X0/0b`3]00Il0606F0241S00[0H<0
;06102d1O`0_0Gh0<`5k03T1N`0n0GX0G@5X02H1QP1J0G00G05_05`1K01N0F/0I@5V06h1I01f0F40
R`5J09l1E`2c0Dh0_05;0`2i0CL0aP550`1B`3/0Dh0k05F0>X1GP3X0FD0i`5Z0>81J`3O0Fl0fP5c0=D1N03A0Gh0d@5l0@1J`3X0FL0l@5N0?41DP3k0DX0lP4n0?`1B@3T0DT0e0590<@1AP2e0DD0
eP5;0<@1B@3/0DT0?00000P000100000600008`0003nooooI`8001X2000U0000300000L0080X0000
30000040000U00003000000008160000500000P00017A4U30`0000`0000@000000000000000U0000
300000D0080U0000300000P0080[0000600006P1000@0@00A`800;<1000U000030000000080U0000
300000L0081B0000L040004000000000000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000000000000300100000004000010000
0@00000000000000000000000@3oool00000800000000000000000000000000000000000000e9@00
000800000000000000000000000000000@000040000100000@000080000200000000000000010000
0@000000000000000@00000000000000000100000000000000010000002L78@2`1b40P3Y4`1N_98`
P0000040001TMP08000002D0000<00000@0001P0000<000000000QT0000<0000oooo0Q/0000@0000
00000000001B0000L0400080003Eoooo0000000000000000T04000000000@00R@@1b06T0H@1/0000
000000000000000000000000000000000000000000000000000000000000000000000000bP2/hA<0
57G:0?ea0c000000V403<0l00002000047G:00000010hQ<0fcl3<11ebP000000g77:043R4`2[A0<`
N1<1SAdl0c0U?0<`H00004P0001P0000B00006cS4`1P0000B000060000180000AG`2<0L0001P0000
000003CR4`2B>`<`1`0008SS4`1kX8``47G:060000180000H00004P0000@MLX0_>@C0000000288h`N1<1SH3R4`0100004>@C06QabP1di1<0
000002d0001TMP08000002D0000<00000P0002P0000<00000@0001P0000<0000IYT00QT0000<0000
oooo0Q/0000@000000000000000F0000300001P0000B000030000040001D0000Q0000481003T0000
3@8001@1000100000736@EEedd5b0@00?P4000T0001<00000000000000000000oooooooooomP0000
J`1^06l0M`1/06D0I01W06D0000F0000600001P0000M00002P0001P0000H0000600001L0000F0000
30000000000B000030000080000H0000300006JI008I000030000?ooo`8K00004000000000000000
5P0000`0000H00004P0000`000010000E000060000120@005`4007d100170@000@00001`aT5EMM=1
LP40074100030000C00000000000000000000?ooooooooooE00006l0KP0P0000600001P0000<0000
5P0000`0000000004P0000`000020000600000`0001VV@026@0000`0003oool26`00010000000000
000001H0000<000060000180000<00000@0005@0001h0000@P4004X1003;0@00NP4000400000LX1000U000030000000080U0000300000L0080H0000300006JI008I000030000?ooo`8K0000
4000000000000000600000`0001VV@026@0000`0003oool26`00010000000000000001H0000<0000
60000180000<00000@0005@0001T00002P000;@0001[0000i00000400000L0@00
100004`00000000000000000003ooooooooooe@0001]06l0LP1U02@0000H00003P0001P0000F0000
30000000000B000030000080000H0000300006JI008I000030000?ooo`8K00004000000000000000
5P0000`0000H00004P0000`000010000E00008@0000:0000i`000=D0000G0@000@00001`aT5EMM=1
>P00044100090000C00000000000000000000?ooooooooooH00006/0KP1_07L0K01U06@0I`1U0000
5P0001P0000H00007@0000X0000H0000600001P0000G00005P0000`0000000004P0000`000020000
600000`0001VV@026@0000`0003oool26`00010000000000000001H0000<000060000180000<0000
0@0005@0001P00002P0001X100150000BP4000400000L0@00M`0007h1000100000736@EEedd4j0000Z04000D0001<0000
0000000000000000oooooooooomH0000K@1_0780I@0P0000900001P0000>0000600000`0000F0000
30000000000B000030000080000H0000300006JI008I000030000?ooo`8K00004000000000000000
5P0000`0000H00004P0000`000010000E00007P0000:0000P@4009<0002a0@000@00001`aT5EMM=1
>P000=/100070000C00000000000000000000?ooooooooooG00006h0K`1d06T0K`1^07<0000H0000
600000`000090000600001L0000F00005P0000`0000000004P0000`0000200004P0000`000020000
3000010000000000000002D0000<00002000P2D0000<00001@00P2D0000<00003@00P2P0000<0000
0P0000h0000D000000000100000D0000
\>"], "Graphics",
ImageSize->{278.813, 248.688},
ImageMargins->{{109.25, 0}, {0, 0}},
ImageRegion->{{0, 1}, {0, 1}}]
}, Open ]],
Cell[CellGroupData[{
Cell["Mathematical Theory Exploration", "Subsubsection"],
Cell[TextData[{
"Starting from a body of knowledge on some concepts ",
StyleBox["(e.g. +, * on numbers and functions)",
FontColor->RGBColor[0, 0, 1]]
}], "Text"],
Cell[TextData[{
"invent (axioms, definitions for) new concepts (operations: predicates, \
functions) ",
StyleBox["(e.g. limit)",
FontColor->RGBColor[0, 0, 1]]
}], "Text",
CellDingbat->"\[EmptySmallCircle]",
CellMargins->{{46.625, Inherited}, {Inherited, Inherited}}],
Cell["invent and prove properties of notions", "Text",
CellDingbat->"\[EmptySmallCircle]",
CellMargins->{{46.625, Inherited}, {Inherited, Inherited}}],
Cell["invent problems about notions", "Text",
CellDingbat->"\[EmptySmallCircle]",
CellMargins->{{46.625, Inherited}, {Inherited, Inherited}}],
Cell["\<\
invent methods (algorithms) for problems and prove their correctness\
\>", "Text",
CellDingbat->"\[EmptySmallCircle]",
CellMargins->{{46.625, Inherited}, {Inherited, Inherited}}],
Cell["compute (apply algorithms to data)", "Text",
CellDingbat->"\[EmptySmallCircle]",
CellMargins->{{46.625, Inherited}, {Inherited, Inherited}}],
Cell["organize, store, and retrieve knowledge", "Text",
CellDingbat->"\[EmptySmallCircle]",
CellMargins->{{46.625, Inherited}, {Inherited, Inherited}}],
Cell["\<\
Current computer algebra systems support some of these aspects.\
\>", "Text"],
Cell["\<\
Current reasoning systems support some other of these aspects.\
\>", "Text"],
Cell[TextData[{
"Goal: Support all these aspects.\nCalculemus, MKM etc. are research \
networks that aim at creating integrated systems. \nGroup members: MIZAR, \
OMEGA, EDIN, ISABELLE, NUPRL, ...\n",
StyleBox["Theorema",
FontSlant->"Italic"],
" is one of the (founding) groups of these networks. "
}], "Text"]
}, Open ]],
Cell[CellGroupData[{
Cell["A Never Ending Endeavor on Two Floors", "Subsubsection"],
Cell[CellGroupData[{
Cell[GraphicsData["Metafile", "\<\
CF5dJ6E]HGAYHf4PEfU^I6mgLb15CDHPAVmbKF5d0@0000oD0@0006`0003oooook_ooofT3002M0P00
00000000000FEP00?dD00215CDH00040e0l0060000040000000000000000000000@00003003n0000
b`000000000000000000033P0`3h60<02P000100000e00005@0000T0000@0000M@<009h2000D0000
300000d000160000:00001`00017A4U30P000;d0000b0000T`8004@200000000G`0003P000010000
>0000000000h0000000000020@090000000009W<0000000000000000000U000030000040000U0000
300000D0080k0000200001/0000@0000>P4005L1001H0000n080000000000000oooooooooong0000
?`540DL1<@5A0Al1E@4F0Ed11@5T0Oh0I`7k07H1lP1k0Nl0Q07Y08P1h@2C0M`0Y`7D0;X1cP3@0LT0
0@;?0382e`1S0]`0I0;O06H2h`1W0^H0J@;Y06/2k01]0^l0M@810G/26P690RP1T@9?0HX2M05o0YX1
OP:V0Gh2/`5k0[l1N`;20GL2`P5f0/@1K`;>0GL2c@5X0]81G@;F0E82f@570]`1A0;P0D42iP4m0^T1
>`;/0CL2k@4d0^l1<0;b0Bh2m`4Z0_P160800PT22`;k0AT2nP4N0_/190;g0BP2l`4[0^d1:P;X0B`2
``4h0_@1:P;<0CD2[0570XH1>P9T0CH2G@4e0TH1<08n0Bd2=P4Z0RL1908W0B@2704=0Qh1408:0@L2
1`440PD100810Oh1o@3l0OD0n07b0?@1j`3^0Ml0h@7O0>41gP3N0Md0f`7K0=P1f03D0M<0d`7A0l0fP3V0=d0f`3S0=<0i03A0>L0d03X0/0b`3]00Il0606F0241S00[0H<0
;06102d1O`0_0Gh0<`5k03T1N`0n0GX0G@5X02H1QP1J0G00G05_05`1K01N0F/0I@5V06h1I01f0F40
R`5J09l1E`2c0Dh0_05;0`2i0CL0aP550`1B`3/0Dh0k05F0>X1GP3X0FD0i`5Z0>81J`3O0Fl0fP5c0=D1N03A0Gh0d@5l0@1J`3X0FL0l@5N0?41DP3k0DX0lP4n0?`1B@3T0DT0e0590<@1AP2e0DD0
eP5;0<@1B@3/0DT0?00000P000100000600008L0000L0000HP8003P2000U0000300000L0080X0000
30000040000U00003000000008160000500000P00017A4U30`0000`0000@00000000000000160000
:00001`00017A4U30P0003D0000D0000eP800;<200000000G`0003P000010000>0000000000h0000
000000020@09000000000?mV0000000000000000000U000030000040000U0000300000D0080k0000
200001/0000@0000R@8009l0001H0000D080000000000000oooooooooon=0000S0:R0902Y02B0ZP0
U0:Z09@2[`2F0[40V`:d0:02]@2U0[H0[@:n0:h2b@2c0]<0`@;^00Y/240:B0QT2R@8R0X82:P9f0S42
K`910Vl2>P9S0T@2H0970Uh2C09J0Td2C`9A0T@2D08i0U42<@9D0RP2EP8Q0U/25@9S0Q/2I@8>0VX2
209/0P42K@;k0Fh2l05l0]`1QP;<0HX2_P6B0[41V@:R0Id2U`6X0U`1ZP9=0J`2=`6Y0R81Y`8>0Il2
2P6J0PH1U0810I02nP2;0^T0R0;T08H2f`230]@0OP;<07T2b`1d0/X0KP;806X2a@1T0[80G`:/05`2
X01A0YP0AP::0402QP0k0X@0=P:00342O@0/0WH0:@9c02@2K@0J0VH0509P00/2F03a0E40fP5=0;l1
B01m0D00>`4j0?T0@@3G03l0]01A09H0FP1f04h0TP1O08<0I01n06@0M@1X0700K@1Y07D0I01k05d0
QP1B08l0A`2M0440Y@0f09/0@@2Z03L0[00f0:h0<`2`0380]P0^0;`0;03302P0a00X0=H08@3F01l0
eP0L0`<`1`0008SS4`1kX8``47G:060000180000H00004P0000@MLX0_>@C0000000288h`N1<1SH3R4`0100004>@C06QabP1di1<0
000002d0001TMP08000002D0000<00000P0002P0000<00000@0001P0000<0000ofH00QT0000<0000
oooo0Q/0000@000000000000000F0000300001P0000B000030000040001D0000Q0000:d2001Z0@00
J@<009X1000100000736@EEedd7R0P00YP4000T0001<00000000000000000000oooooooooomP0000
LP1U0640L`1_06h0I@1b07<0000>0000600001P0000E0000600001P0000H00003@0001D0000F0000
30000000000B000030000080000B000030000080000<00004000000000000000AP0002P0000L0000
AdA9@`80001o0P00S`400<82002j0@00000005l0000h00000@0003P000000000>000000000000040
0@0000000000000000000000000000009@0000`0000100009`0001P00003000000000?mV00000000
9@0000`000030000EP0003P000190P00N@4008d2002U0@001`000902T06@0YX1`0:J0L02[P6@0Zh1
T0:h0H02Y04U0000300000L0080X000030000040000U000030000000080X0000300000<000160000
500000P00017A4U30`0000`0000@00000000000000160000:00001`00017A4U30P000001000f0P00
<`4007L200000000G`0003P000030000>0000000000h0000000000000@0100000000000000000000
00000000000U0000300000<0000W00006000004000000000ofH00000000U000030000040001F0000
>00000RP1BP8C0GD20@5]0QH1@@8=0Cd29P4g0RD0000<0000
1`00P2P0000<00000`0002D0000<00000000P2P0000<00000@0004H0000D0000200004M4BD<30000
3000010000000000000004H0000X0000700004M4BD<20000gP4002l2000B0P00K`800000001O0000
>0000040000h0000000003P00000000000010040000000000000000000000000000002D0000<0000
0@0002L0000H00000`000000003oIP00000002D0000<00000`0005H0000h0000Z04001T2003M0@00
FP8000L000020S@2n@4i0Q02I0;n0Fd2j0530]l1A`;Y0C029@0000`000070020:00000`000010000
9@0000`000000020:00000`000030000AP0001@000080000AdA9@`<0000<00004000000000000000
9@0000`0000800209@0000`0000500209@0000`0000=0020:00000`0000200003P0001@000000000
400001@0
\>"], "Graphics",
ImageSize->{310.625, 244.188},
ImageMargins->{{74, 0}, {0, 14.5}},
ImageRegion->{{0, 1}, {0, 1}}],
Cell[GraphicsData["Metafile", "\<\
CF5dJ6E]HGAYHf4PEfU^I6mgLb15CDHPAVmbKF5d0@0001<@0@0006`0000:0000k_oooiD3002M0P00
00000000001NFP00?dD00215CDH0004041<008H000040000000000000000000000@00003003n0000
b`000000000000000000033P0`3h60<02P000100000P0000>@0000T0000@0000X@<009h2000D0000
300000d000160000:00001`00017A4U30P0001D1001F0000j`8006P200000000G`0003P000010000
>0000000000h0000000000020@090000000009W<0000000000000000000U000030000040000U0000
300000D0080k0000200001/0000@0000TP4007/1001H0000n080000000000000oooooooooong0000
U`5W0Il1E@6Y0D81[@4j0KD1:@6l0B81_`4N0Lh15P7C0A<1g04=0N011@7[0@01o`7h0182lP0X0^d0
F@;c08X2n`2k0P01_0830Kh21`6o0PX1`@8=0L<240750Q<1c@8U0M<2?@7Q0T`1j@9b0N82V07G0[d1
eP;:0MH2e`7C0^<1d`;U0Ll2iP7>0^L1a`;b0Ll2l@700_H1]@;j0JX2o@6O0P02W0840YT22@:E0Pd2
T`8@0Xl240:<0Q<2R08E0XH26P:20Q`2L08T0V42;`9C0Sd2DP920U<2B09?0T/2B`9?0TD2CP900Tl2
6`9L0T`2CP8T0UT2109[0]h1GP:l0EX2]@5I0Yh1E0:F0E42SP5>0Wl1A`9o0DL2M04a0WH1=09R0B/2
G`4X0Ud1909I0B42E@4O0Td16`9:0AP2@`4B0SL11@8g0@D2=P420SD1oP4c0O`1<07h0B/1mP4Y0O81
907S0BD1dP4P0L<17P6S0A/1Q04K0F@16P550B01;P4^0A<10MX0E07C05X1c@1Q0LL0H`7606D1a@1V0L<0L06j07T1/0230JL0
Q06U08D1XP270J40R`6O0941W`2F0Id0]@6<07h1Z@2b0I@0]06C0;@1T02f0Hl0_@6:00HD0
h`5n0?L1NP0;0W80509_01h2L00X0Vh0;P9]03@2J`0k0VT0;09T01l2G`0A0U/07P9X0282I@0k0VT0
?@9Z04@2K`140W80A09j0482PP100XT0?`:>03X2S`0g0Y<00000000000h0000
000000020@09000000000?mV0000000000000000000U000030000040000U0000300000D0080k0000
200001/0000@0000h@800<<0001H0000D080000000000000oooooooooon=0000i0;60>P2b03Z0//0
k0;>0>`2d`3^0]D0l`;H0?P2f03m0]X01@?R00H3k@0;0oL06@20BH3]`4S0nd1
8`?h0B03n@4J0`02500UD2
a`9T0/L2GP:k0VP2^09[0[H2L0:b0W42Y`9e0Y`2M0:A0WD2R@9h0X02NP9i0Wl2K@:70W<2R@9V0Xh2
H0:@0UT2T09C0Y82B0:P0S@2ZP8T0Zh25P:f0PT2_@;j0L42k`7<0[@1cP:U0M02S`7=0WX1b`9V0L82
HP6n0Uh1]`9I0K@2DP6_0T41[08l0JX2<`6W0R`1XP8T0Id28`6H0R81TP8P0Hh27@680PX1P`840H02
n01e0_00JP;R06@2gP1O0]`0FP;H05D2e@1@0/h0C@;;04L2a@0n0[h0>0:h02l2/00E0ZT0oP6U0><1
X02Q0IP0G`6B01d1V@3k09L0f02Y0;X0/P2J0:H0]P2g0:L0_02R0;`0V@3009@0a@2=0L0J`3e06D0o@1I0?<0I@020E/0105J00H1E`080EH03P5B01@1C`0K0D`0705<02h1A@0^0D<0
;P4o02L1AP0T0DL0;`5E0281J@0K0GH0705i01`1OP0O0H008@6102<1OP0T0G`0:05a02h1F`0^0E/0
9P4]0381@`3W04<0?00000P000100000600006`0003^oooo3@<009d2000U0000300000L0080X0000
30000040000U00003000000008160000500000P00017A4U30`0000`0000@000000000000000U0000
300000D0080U0000300000P0080[000060000>l2002`0000`0<00>d0000U000030000000080U0000
300000L0081B0000L040004000000000000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000000000000000000000000000000000
00000000000000000000000000000000000000000000000000000000000300100000004000010000
0@00000000000000000000000@3oool00000800000000000000000000000000000000000000e9@00
000800000000000000000000000000000@000040000100000@000080000200000000000000010000
0@000000000000000@00000000000000000100000000000000010000000`0H@2E0640P3Y4`1N_98`
P0000040001TMP08000002D0000<00000@0001P0000<000000000QT0000<0000oooo0Q/0000@0000
00000000001B0000L0400080003Eoooo0000000000000000T04000000000@00R@@1b06T0H@1/0000
000000000000000000000000000000000000000000000000000000000000000000000000bP2/hA<0
57G:0?ea0c000000V403<0l00002000047G:00000010hQ<0fcl3<11ebP000000g77:043R4`2[A0<`
N1<1SAdl0c0U?0<`H00004P0001P0000B00006cS4`1P0000B000060000180000AG`2<0L0001P0000
000003CR4`2B>`<`1`0008SS4`1kX8``47G:060000180000H00004P0000@MLX0_>@C0000000288h`N1<1SH3R4`0100004>@C06QabP1di1<0
000002d0001TMP08000002D0000<00000P0002P0000<00000@0001P0000<0000ofH00QT0000<0000
oooo0Q/0000@000000000000000F0000300001P0000B000030000040001D0000Q0000=T2001n0000
U@<00:h0000100000736@EEedd7i0P00gP0000T0001<00000000000000000000oooooooooomP0000
LP1U0640L`1_06h0I@1b07<0000>0000600001P0000E0000600001P0000H00003@0001D0000F0000
30000000000B000030000080000B000030000080000<00004000000000000000AP0002P0000L0000
AdA9@`80003G0P00/`4001X3003N0@00000005l0000h00000@0003P000000000>000000000000040
0@0000000000000000000000000000009@0000`0000100009`0001P00003000000000?mV00000000
9@0000`000030000EP0003P0002f0P00N@400?X2002U0@001`000>P2]07X0[h160>n0AP3dP7X0]81
j0;L0MP2b04U0000300000L0080X000030000040000U000030000000080X0000300000<000160000
500000P00017A4U30`0000`0000@00000000000000160000:00001`00017A4U30P0005P1001J0P00
R`4009/200000000G`0003P000030000>0000000000h0000000000000@0100000000000000000000
00000000000U0000300000<0000W00006000004000000000ofH00000000U000030000040001F0000
>00003L1000P0P00J`40068200070000R@5b0X01KP9[0IT2F@6@0Vh1I@9U0F42OP5K0RD0000<0000
1`00P2P0000<00000`0002D0000<00000000P2P0000<00000@0004H0000D0000200004M4BD<30000
3000010000000000000004H0000X0000700004M4BD<20000=P8005<2001Z0P00T`800000001O0000
>0000040000h0000000003P00000000000010040000000000000000000000000000002D0000<0000
0@0002L0000H00000`000000003oIP00000002D0000<00000`0005H0000h00005@8001T2001:0P00
FP8000L0001J0UP2D@9M0VP2Q`9F0Y42@09V0SL2J`910U@29@0000`000070020:00000`000010000
9@0000`000000020:00000`000030000AP0001@000080000AdA9@`<0000<00004000000000000000
AP0002P0000L0000AdA9@`8000370000>`4000X1001V0@00000005l0000h00000`0003P000000000
>0000000000000400@0000000000000000000000000000009@0000`0000300009`0001P000010000
000006JI000000009@0000`000010000EP0003P0002V00000@400>X0000]0@001`000=P0?07H04H1
20560@P1FP7H05X1f01T0LP0D04U0000300000L0080X0000300000<0000U000030000000080X0000
3000004000160000500000P00017A4U30`0000`0000@000000000000000U0000300000D0080U0000
300000P0080[000060000200001H0000l@0000000600001P0000E0000600001P0000H00003@0001D0000F0000
30000000000B000030000080000B000030000080000<000040000000000000009@0000`000080020
9@0000`0000500209@0000`0000=0020:00000`0000200003P0001@000000000400001@0
\>"], "Graphics",
ImageSize->{331.125, 250.875},
ImageMargins->{{58, 0}, {0, 20.625}},
ImageRegion->{{0, 1}, {0, 1}}]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell[TextData[{
"Integration in ",
StyleBox["Theorema",
FontSlant->"Italic"],
" "
}], "Subsubsection"],
Cell["Integration in one logic: a version of predicate logic.", "Text"],
Cell["\<\
Integration in one software system: implementation language (\"meta \
language\") is Mathematica:\
\>", "Text"],
Cell[TextData[{
"A. Mathematica as a programming language (",
StyleBox["Theorema",
FontSlant->"Italic"],
" reasoners are programmed in Mathematica)"
}], "Text",
CellMargins->{{70, Inherited}, {Inherited, Inherited}}],
Cell["\<\
B. Mathematica as a front-end (flexible syntax, hierarchical notebooks, \
graphics etc.)\
\>", "Text",
CellMargins->{{70, Inherited}, {Inherited, Inherited}}],
Cell[TextData[{
"(In the future, we may use ",
StyleBox["Theorema",
FontSlant->"Italic"],
" for A.)"
}], "SmallText"]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell["Syntax and Manipulating Mathematical Texts", "Section"],
Cell[CellGroupData[{
Cell["Initialize Theorema", "Subsubsection"],
Cell[CellGroupData[{
Cell[BoxData[
\(\(Needs["\"];\)\)], "Input"],
Cell[BoxData[
\("You can specify your personal preferences in a file `Setup.m` in the \
directory (folder) \"Theorema -> User\" in your private Theorema \
directory!"\)], "Print"]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell["Predicate Logic Formulae, Labels, and Keywords", "Subsubsection"],
Cell[BoxData[
RowBox[{
StyleBox["Definition",
FontWeight->"Bold"], "[", \("\", any[f, a], \n\t
limit[f, a]\[DoubleLongLeftRightArrow]\ \(\(\[ForAll] \
\+\[Epsilon]\)\+\(\[Epsilon] > 0\)\(\[Exists] \+N\(\(\[ForAll] \+n\)\+\(n \
\[GreaterEqual] N\)\[LeftBracketingBar]f[n] -
a\[RightBracketingBar] < \[Epsilon]\)\)\)\),
"]"}]], "Input",
CellTags->"Definition (limit:)"],
Cell[TextData[{
"Note that logic \"application\" is denoted by brackets in ",
StyleBox["Theorema",
FontSlant->"Italic"],
"!"
}], "Text"],
Cell[BoxData[
\(Definition["\"]\)], "Input"],
Cell[BoxData[
\(Definition["\"]\ // InputForm\)], "Input"],
Cell[TextData[{
"The identifier spaces of ",
StyleBox["Theorema",
FontSlant->"Italic"],
" and Mathematica are kept disjoint!"
}], "Text"],
Cell[BoxData[
\(limit[f,
a]\[DoubleLongLeftRightArrow]\ \(\(\[ForAll] \+\[Epsilon]\)\+\(\
\[Epsilon] > 0\)\(\[Exists] \+N\(\(\[ForAll] \+n\)\+\(\(\[ForAll] \
\+\[Epsilon]\)\+\(\[Epsilon] > 0\)\(\[Exists] \+N\(\(\[ForAll] \+n\)\+\(n \
\[GreaterEqual] N\)\[LeftBracketingBar]f[n] - a\[RightBracketingBar] < \
\[Epsilon]\)\)\)\[LeftBracketingBar]f[n] -
a\[RightBracketingBar] < \[Epsilon]\)\)\)\)], "Input"],
Cell["Users can program their own syntax!", "Text"],
Cell[BoxData[
RowBox[{
StyleBox["Proposition",
FontWeight->"Bold"], "[", \("\",
any[f, a, g,
b], \n\t\((limit[f, a] \[And]
limit[g, b])\)\ \ \ \ \ \[Implies] \ \ \ \ \ limit[f + g,
a + b]\), "]"}]], "Input",
LimitsPositioningTokens->{},
CellTags->"Proposition (limit of sum)"],
Cell[BoxData[
RowBox[{
StyleBox["Definition",
FontWeight->"Bold"], "[", \("\<+:\>",
any[f, g, x], \n\t\((f + g)\)[x] = f[x] + g[x]\), "]"}]], "Input",
LimitsPositioningTokens->{},
CellTags->"Definition (+:)"],
Cell[BoxData[
RowBox[{
StyleBox["Lemma",
FontWeight->"Bold"], "[", \("\<|+|\>",
any[x, y, a,
b, \[Delta], \[Epsilon]], \n\t\((\[LeftBracketingBar]\((x +
y)\) - \((a +
b)\)\[RightBracketingBar] < \((\[Delta] + \
\[Epsilon])\))\)\ \ \ \ \[DoubleLongLeftArrow]\ \ \ \((\[LeftBracketingBar]x \
- a\[RightBracketingBar] < \[Delta] \[And] \[LeftBracketingBar]y -
b\[RightBracketingBar] < \[Epsilon])\)\), "]"}]], "Input",
LimitsPositioningTokens->{},
CellTags->"Lemma (|+|)"],
Cell[BoxData[
RowBox[{
StyleBox["Lemma",
FontWeight->"Bold"], "[", \("\", any[m, M1, M2], \n\t
m \[GreaterEqual]
max[M1, M2]\ \ \ \ \ \[Implies] \ \ \ \ \ \((m \[GreaterEqual]
M1 \[And] m \[GreaterEqual] M2)\)\), "]"}]], "Input",
LimitsPositioningTokens->{},
CellTags->"Lemma (max)"]
}, Open ]],
Cell[CellGroupData[{
Cell["Combining Formulae to \"Theories\"", "Subsubsection"],
Cell[BoxData[
RowBox[{
StyleBox["Theory",
FontWeight->"Bold"], "[",
RowBox[{"\"\\"", ",", "\n", "\t", GridBox[{
{
RowBox[{
StyleBox["Definition",
FontWeight->"Bold"], "[", "\"\\"", "]"}]},
{
RowBox[{
StyleBox["Definition",
FontWeight->"Bold"], "[", "\"\<+:\>\"", "]"}]},
{
RowBox[{
StyleBox["Lemma",
FontWeight->"Bold"], "[", "\"\<|+|\>\"", "]"}]},
{
RowBox[{
StyleBox["Lemma",
FontWeight->"Bold"], "[", "\"\\"", "]"}]}
},
ColumnAlignments->{Left}]}], "]"}]], "Input",
LimitsPositioningTokens->{},
CellTags->"Theory (limit)"],
Cell[CellGroupData[{
Cell[BoxData[
\(Theory["\"]\)], "Input"],
Cell[BoxData[
RowBox[{"\[Bullet]thr", "[",
RowBox[{"\<\"limit\"\>", ",", \(\[Bullet]range[]\), ",", "True", ",",
RowBox[{"\[Bullet]flist", "[",
RowBox[{
RowBox[{"\[Bullet]def", "[",
RowBox[{"\<\"limit:\"\>", ",",
RowBox[{"\[Bullet]range", "[",
RowBox[{
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["f",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["a",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}]}], "]"}], ",", "True", ",",
RowBox[{"\[Bullet]flist", "[",
RowBox[{"\[Bullet]lf", "[",
RowBox[{"\<\"\"\>", ",",
RowBox[{
RowBox[{"limit", "[",
RowBox[{
StyleBox["f",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], ",",
StyleBox["a",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], "]"}],
"\[DoubleLeftRightArrow]",
RowBox[{
UnderscriptBox[
UnderscriptBox["\[ForAll]",
RowBox[{
StyleBox["\[Epsilon]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], " "}]],
RowBox[{
StyleBox["\[Epsilon]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], ">", "0"}]],
RowBox[{
UnderscriptBox["\[Exists]",
RowBox[{
StyleBox["N",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], " "}]],
RowBox[{
UnderscriptBox[
UnderscriptBox["\[ForAll]",
RowBox[{
StyleBox["n",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], " "}]],
RowBox[{
StyleBox["n",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "\[GreaterEqual]",
StyleBox["N",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}]],
RowBox[{"(",
RowBox[{
RowBox[{"\[LeftBracketingBar]",
RowBox[{
RowBox[{
StyleBox["f",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "[",
StyleBox["n",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], "-",
StyleBox["a",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}],
"\[RightBracketingBar]"}], "<",
StyleBox["\[Epsilon]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], ")"}]}]}]}]}]}],
"]"}], "]"}]}], "]"}], ",",
RowBox[{"\[Bullet]def", "[",
RowBox[{"\<\"+:\"\>", ",",
RowBox[{"\[Bullet]range", "[",
RowBox[{
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["f",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["g",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}]}], "]"}], ",", "True", ",",
RowBox[{"\[Bullet]flist", "[",
RowBox[{"\[Bullet]lf", "[",
RowBox[{"\<\"\"\>", ",",
RowBox[{
RowBox[{
RowBox[{"(",
RowBox[{
StyleBox["f",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "+",
StyleBox["g",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], ")"}], "[",
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], "=",
RowBox[{
RowBox[{
StyleBox["f",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "[",
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], "+",
RowBox[{
StyleBox["g",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "[",
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}]}]}]}], "]"}], "]"}]}],
"]"}], ",",
RowBox[{"\[Bullet]lma", "[",
RowBox[{"\<\"|+|\"\>", ",",
RowBox[{"\[Bullet]range", "[",
RowBox[{
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["y",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["a",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["b",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["\[Delta]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["\[Epsilon]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}]}], "]"}], ",", "True", ",",
RowBox[{"\[Bullet]flist", "[",
RowBox[{"\[Bullet]lf", "[",
RowBox[{"\<\"\"\>", ",",
RowBox[{
RowBox[{
RowBox[{"\[LeftBracketingBar]",
RowBox[{
RowBox[{"(",
RowBox[{
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "+",
StyleBox["y",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], ")"}], "-",
RowBox[{"(",
RowBox[{
StyleBox["a",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "+",
StyleBox["b",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], ")"}]}],
"\[RightBracketingBar]"}], "<",
RowBox[{
StyleBox["\[Delta]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "+",
StyleBox["\[Epsilon]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}]}], "\[DoubleLeftArrow]",
RowBox[{"(",
RowBox[{
RowBox[{
RowBox[{"\[LeftBracketingBar]",
RowBox[{
StyleBox["x",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "-",
StyleBox["a",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}],
"\[RightBracketingBar]"}], "<",
StyleBox["\[Delta]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], "\[And]",
RowBox[{
RowBox[{"\[LeftBracketingBar]",
RowBox[{
StyleBox["y",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "-",
StyleBox["b",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}],
"\[RightBracketingBar]"}], "<",
StyleBox["\[Epsilon]",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}]}], ")"}]}]}], "]"}],
"]"}]}], "]"}], ",",
RowBox[{"\[Bullet]lma", "[",
RowBox[{"\<\"max\"\>", ",",
RowBox[{"\[Bullet]range", "[",
RowBox[{
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["m",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["M1",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}], ",",
RowBox[{"\[Bullet]simpleRange", "[",
StyleBox["M2",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "]"}]}], "]"}], ",", "True", ",",
RowBox[{"\[Bullet]flist", "[",
RowBox[{"\[Bullet]lf", "[",
RowBox[{"\<\"\"\>", ",",
RowBox[{
RowBox[{
StyleBox["m",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "\[GreaterEqual]",
RowBox[{"max", "[",
RowBox[{
StyleBox["M1",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], ",",
StyleBox["M2",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], "]"}]}], "\[Implies]",
RowBox[{
RowBox[{
StyleBox["m",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "\[GreaterEqual]",
StyleBox["M1",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}], "\[And]",
RowBox[{
StyleBox["m",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None], "\[GreaterEqual]",
StyleBox["M2",
FontWeight->"Plain",
FontSlant->"Italic",
Background->None]}]}]}]}], "]"}], "]"}]}],
"]"}]}], "]"}]}], "]"}]], "Output"]
}, Open ]],
Cell[BoxData[
RowBox[{"Theory", "[",
RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{
{\(Theory["\"]\)},
{\(\(Lemma["\"]\)\(\ \)\)}
},
ColumnAlignments->{Left}]}], "]"}]], "Input",
CellTags->"Theory (Test)"]
}, Open ]],
Cell[CellGroupData[{
Cell["\<\
Logicographic Symbols (Invent Arbitrary New Symbols and Two-dimensional \
Nesting)\
\>", "Subsubsection"],
Cell[TextData[{
"Logicographic Symbols: ",
"In ",
StyleBox["Theorema",
FontSlant->"Italic"],
", users can invent, design, declare, and use their own mathematical \
symobls:"
}], "Text"],
Cell[GraphicsData["Bitmap", "\<\
CF5dJ6E]HGAYHf4PAg9QL6QYHg0P83oooook_ooo`00oooooooooooooooooooooe7ooomSP820oooo
onkoool00?oooooooooooooooooooomAooooHh20P?ooooo^oooo003ooooo
ooooooooooooooooDOooof>0P83oooook_ooo`00oooooooooooooooooooo
oe7ooomSP820ooooonkoool00?oooooooooooooooooooomAooooHh20P?oo
ooo^oooo003oooooooooooooooooooooDOooof>0P83oooook_ooo`00oooo
oooooooooooooooooe7ooomSP820ooooonkoool00?oooooooooooooooooo
oomAooooHh20P?ooooo^oooo003oooooooooooooooooooooDOooof>0P83o
ooook_ooo`00oooooooooooooooooooooe7ooomSP820ooooonkoool00?oo
oooooooooooooooooomAooooHh20P?ooooo^oooo003ooooooooooooooooo
ooooDOooof>0P83oooook_ooo`00oooooooooooooooooooooe7ooomSP820
ooooonkoool00?oooooooooooooooooooomAooooHh20P?ooooo^oooo003o
ooooooooooooooooooooDOooof>0P83oooook_ooo`00oooooooooooooooo
oooooe7oool4P820Flcoooo]X20P?ooooo;oooo1820P0CcLc0P83oooook_ooo`00oooo
ogKoool30000EOoooe60P807c0P83oooook_ooo`00ooooogKoool30000EOoooe60P805c0P83oooook_ooo`00ooooogKo
ool30000EOooo`V0P80X00008820P0Oc00003?oo
o`030000oooooooo00Goool00`000?ooooooo`08oooo3`0000Soool20000
00?oool0000000001P0000koool90000/?ooob20P80600003820P0H0000;
P820100001b0P83oooook_ooo`00ooooogKoool30000EOooo`V0P8040000
5H20P0X0000UP8202lc
oooo2`0000Goool700001Oooo`L00006oooo3P0000Goool>00002oooo`80
0007oooo0P0000Woool?00001oooo`h0000:oooo3P000:gooolQP8201`00
00V0P80600002h20P0D0000LP820ooooonkoool00?oooomfoooo0`0005Go
ool9P820100001>0P80:00009h20P0_00002oooo`h00003oooo1`0000Goool700001?oooa400004oooo
3P0000_oool300001Oooo`<00009oooo3`0000Ooool?00001ooooa40002/
oooo8X20P0L00006P8201`0000^0P80600007820P?ooooo^oooo003ooooo
M_ooo`<0000Coooo1P0000;oool70000coooo0P00
00[oool300001?ooo`<0002loooo9X20P0`0000;P8201`0001n0P83ooooo
k_ooo`00ooooogKoool300005_ooo`H00005oooo1@0002ooool4P820;@00
0220P80>c0P804
00000X20P0X00005P8202`0008f0P80Roooo1@0003Koool300002_ooo`<0
0009oooo0`00017oool300002Oooo`<00004oooo100000_oool300002Ooo
o`@0000?oooo0P0000Coool300001?ooo`80000=oooo0`0000koool50000
3_ooo`@0000;oooo0`000:gooolVP820300000F0P80700009H20P0Woool3
0000ooooon;oool00?oooomfoooo0`0001Koool300002oooo`<00000P80>00001H20P0/0002?P8208_ooo`D0000f
oooo100000Soool400002Oooo`<0000Aoooo100000Soool300001Oooo`@0
0009oooo100000Woool600001_ooo`800004oooo0`0000Goool200001?oo
o`<00000P80000000000100000>0P80700009X20P0Woool3
0000ooooon;oool00?oooomfoooo0`0001Koool300002oooo`<00000P80:00001H20P0/0000BP8203/cc0P80600001820P0/0000GP8203Lc
00009h20P0Woool300004?ooo`80003oooood?ooo`00JooookN0P81Coooo
0`0001Koool30000??ooo`B0P80200001820P0/0000PP8202/coooo1P0005[oool30000h?oooa^0P80600002h20P0H00005
P8201`0002F0P809oooo0`00013oool30000ooooolooool006_ooolfP820
3/c3ooolJP8201P0000^0P8060000
2820P0H0000TP8202Oooo`<0000Aoooo0`000?ooooo>oooo001[oooo=X20
P0goooo001[oooo=X20P0gc0P809oooo0`000?oooooRoooo001[
oooo=X20P0S0
P809oooo0`000?oooooRoooo001[oooo=X20P0Scc00005_ooo`@0001Foooo]X20P?ooooo;oooo2820P0W0P80300002h20P0@00002P8201LcP820Boooo`L0003ooooo
ooooom_oool8P8202Lc0P80?
00001H20P0G0P80<0000
1X20P0X0002BP820Boooo`L0003oooooooooom_oool8P8202Lc0P80:00001X20P0X0000CP820O0P80300002X20P0@00003P8201Lcc00005Oooo`@0001Goooo]h20
P?ooooo:oooo2820P0W0P805c0P80300002h20P0<00003P8201Lcc0P805ccccc
ccP8202`0000n0
P80LcLcOooo`/0000G
oooo1`0001koool300002oooo`<0003ooooo4_ooof>0P83oooook_ooo`00
ooooogKoool300005_ooo`l0000?oooo300001Goool4P8200P0000>0P804
00000X20P0X00005P8202`0008j0P80Qoooo1@0004;oool300006Oooo`L0
000Loooo100000Woool40000oooooa;ooomSP820ooooonkoool00?oooomf
oooo0`0001Soool=00003_ooo`h0000Doooo1820P0800003P8203P0000F0
P80;0000T820P27oool50000@_ooo`<0000Loooo1P0001[oool500001ooo
o`@0003ooooo4oooof>0P83oooook_ooo`00ooooogKoool300006_ooo`/0
000>oooo0`0000Soool300005?ooo`B0P80200000h20P0`00005P8202`00
02f0P813c0P83oooook_ooo`00ooooogKoool300008_oo
o`<0000>oooo00<0003oooooool02_ooo`030000oooooooo01;oool4P820
0P0000>0P80:00001H20P0/0000_P8203/c0
P83oooook_ooo`00ooooogKoool300008_ooo`<0000`oooo1820P0800003
P820200000B0P80;0000c00000P83oooook_ooo`00oooo
ogKoool300005_ooo`d0000boooo1820P0800003P82000<00020P820P800
0h20P0/0000hP8202lc0P83oooook_ooo`00ooooogKoool3
0000EOooo`B0P80200001820P0/0000mP8202/c0P83oooook_ooo`00ooooogKoool30000EOooo`B0P80=0000@H20P0W<
c<`300002lc0P83oooook_ooo`00ooooogKoool30000EOooo`B0
P80:0000A820P0S0P83ooooo
k_ooo`00ooooogKoool30000EOooo`B0P8040000BX20P0O0P83oooook_ooo`00ooooogKoool3
0000EOoooe:0P805cccoooo
]h20P?oooomKoooo0`000?oooooooooo__ooo`00ooooolkooongP820oooo
oe_oool30000oooooooooonnoooo003oooooc_oookN0P83oooooFoooo`<0
003ooooooooookkoool00?ooooooooooooooon7oool30000oooooooooonn
oooo003ooooooooooooooooQoooo0`000oooo`/0000ioooo0P0004Soool<00004Oooo`P0000Toooo
0P0003Goool800004?ooo`800029oooo001[oooo=H20P2g?ooo`800018oooo
3000017oool800009?ooo`80000eoooo2000013oool20000ROooo`00Jooo
ocF0P80>c00000oooo`L00003oooo1@00
00?oool;00000oooo`D00003oooo1@0000?oool:000000?oool000000000
100000[oool300008?ooo`L00003oooo1@0000?oool500001Oooo`d00005
oooo4@0002;oool400006_ooo`X000000oooo`000000000400000oooo`L0
0005oooo1`0000Woool500004_ooo`<0000:oooo2@0000Koool900002Ooo
o`@0000Foooo4`0000goool300004_ooo`@00025oooo001[oooo=H20P0[<
c<`400004oooo0`0000[oool30000:_ooo`<0000oooo
4`0000Coool300001Oooo`<00005oooo0`0000?oool300001Oooo`<00005
oooo0`0000Koool=00003Oooo`<0000Roooo0`0000Goool300001Oooo`<0
0003oooo0`0000_oool300003?ooo`D00016oooo3@0000Soool300002Ooo
o`<00007oooo0`0000Ooool300003_ooo`<0000?oooo3P0002_oool30000
2Oooo`D0000oooo
100000_oool300001Oooo`<00005oooo0`0000Goool300000oooo`<00005
oooo0`0000Goool300004?ooo`<0000=oooo0`00013oool00`000?oooooo
o`03oooo00<0003oooooool02Oooo`<00005oooo0`0000Goool300000ooo
o`@00009oooo100000ooool400003?ooo`030000oooooooo00?oool00`00
0?ooooooo`0ioooo0`0000Soool300002Oooo`<00006oooo0`0000Woool3
00003Oooo`<0000@oooo0`0000Koool30000;?ooo`l0000>oooo0`0009_o
ool006_oool9P820:00000B0P805c0000
1ooooa000003oooo200000Ooool800002Oooo`<0000Aoooo0`0000?oool3
0000;_ooo`<0000:oooo100000coool30000Voooo`00Joooo`V0P8040000
5820P0/00009P8201lcoooo2`0006[oool300003ooo
o`<00003oooo0`0003Soool500001Oooo`@00009oooo0`0000?oool30000
M_ooo`<0000?oooo2@0002gooolC00003Oooo`<0002Koooo001[oooo1820
P2`00005P8202/coooo
3P0001?oool300002?ooo`<0003oooooooooooooool?oooo2`0006[oool3
00003oooo`<00003oooo0`0003Woool<00002_ooo`<00003oooo0`0007Ko
ool300003oooo`P0000^oooo4@0000ooool30000Voooo`00Joooo`B0P80Z
00001h20P0_00005?ooo`<0
0006oooo0`000?oooooooooooooooa3oool;0000J_ooo`<0000?oooo0`00
00?oool30000>_ooo`X0000;oooo0`0000?oool30000M_ooo`P0000:oooo
200002koool?00003?ooo`P0002Koooo001[oooo1820P2L0000:P8202lc<
c0@0000>cKoool80000Foooo`P0002Koooo001[oooo1820P0800003P820
3`0000F0P80:00003X20P0c0P80:00001X20P0X0000BP8203/c0P80800001H20P0/00015P8207?ooo`<0000>
oooo3P0001Soool40000ooooooooooooooooROooo`<0003oooookOooo`00
Joooo`B0P80200000h20P0H00005P8202`0004N0P80Koooo1@0000goool>
00005oooo`H0003ooooooooooooooon8oooo0`000?ooooo]oooo001[oooo
1820P0800003P8200`0000J0P80;0000BH20P1_oool500000P8000`000820P820P004P8202`0002F0P80Gcoooo0`0000So
ool30000oooooooooooooooooooooooooomeoooo001[oooo1820P0800004
P8202P0002b0P8000lc820P0SH20P0Woooo3P0001Soool30000oooooooooooooooooooooooooomkoooo001[
oooo1820P2X00007P820;Lc0P80400000X20P0/00005P8202P0000b0P80=
c00005_ooo`<000001?ooo`00000000000?oooooo
ooooooooooooooooooooNOooo`00Joooo`B0P80200000h20P0<00006P820
2`0001R0P80:c0P8000`000820P820P004P8202`0001Z0P809ccoooo
100000coooleP820DoooocJ0P8001?ooo`000000000004gooolFP8200P00
00j0P8070000;H20P0P8070000>820P0P80700009H20P1Woool300006oooo`<0
000Ioooo1820P0800003P8201`0002J0P808oooo0`0004Koool4P820D/c<
c0B0P809oooo0`00013oool20000Z_ooo`00oooooooooooooooooooooe[o
ool300004oooo`B0P80200000X20P0L0000VP8206Oooo`<0000Koooo0`00
01Woool4P8200P0000:0P80700009h20P0Soool30000A_ooo`B0P81Bc0P80300003820
P0<00002P8201Lc0P80@00001820P0G0P80?00001H20P0G0P80?
00001H20P0GP8206Lc0P80300002X20P0@00003
P8201LcP8202@0000K
P8200lcP8208Oooo`<0000;oooo0`00027o
ool?P8200lc0P805cP8201LcP8208oooo`<00007oooo0`0002?oool?P8200lcP8201/cP8208oooo`@00005oooo100002?oool?P8200lcP8201/cP8209?oo
o`<00005oooo0`0002Coool?P8200lcP820
1lcP8209?ooo`<00005oooo0`0002Coool?
P8200lcP8201lcP8209?oo
o`@00003oooo100002Coool?P8200lcP8202P8209Oooo`<00003oooo0`0002Goool?P8200lc0P803
00003820P0<00004P8201?ooo`80000Moooo300001Ko
ool800004?ooo`80003oooooAoooo`<0000Coooo3X20P0Soooo``0000Roooo0P0004Soool<00004Oooo`P0000Roooo0P0003Oo
ool20000=oooo`80000goooo0P0003Soool200007Oooo``0000Foooo2000
013oool20000ooooodSoool300004_ooo`j0P809cP820
9_ooo`<000001?ooo`000000000002Koool?P8200lcP8201LcP8209oooo`D0000W
oooo3h20P0l00008c00002Oooo`l0000=oooo1`0000Soool7
00001Oooo`L000000oooo`000000000500000oooo`D00003oooo1@0000Wo
ool300008?ooo`L00003oooo1@0000?oool500001oooo`H00002oooo0`00
02;oool300007Oooo`H00003oooo1P0000?oool700001Oooo`L0000:oooo
100001;oool300002oooo`P00005oooo1`0000[oool300007?ooo`/0000?
oooo0`0001goool600000oooo`H0000:oooo0`0001Ooool600000_ooo`L0
000@oooo0`0001Woool800001Oooo`P00009oooo0`00027oool400007?oo
o`<0000Boooo0`000?oooom5oooo0`0001;oooleP820:?ooo`<0000Xoooo
=X20P0Ooool30000Aoooo`B0P804c00002Oooo`l0000oooo100001Soool800001Oooo`P00009oooo100001ooool500007?oo
o`<0000Boooo10000?oooom5oooo0`00017oooleP820:?ooo`<0000Xoooo
=X20P0Koool30000B?ooo`B0P804c00002Oooo`l0000;oooo3P0000?oool7
00001Oooo`L000000oooo`000000000500000oooo`D00003oooo1@0000Wo
ool300008?ooo`L00003oooo1@0000?oool500000oooo`l0000Roooo1@00
01SooolB00000oooo`L00005oooo1`0000Woool600004Oooo`<0000;oooo
200000Goool700002_ooo`D0000Joooo2`0000ooool500006?oooa80000:
oooo1@0001GooolB00003Oooo`D0000Goooo200000Goool800002Oooo`D0
000Noooo1P0001_oool300004_ooo`D0003oooooA?ooo`<0000Aoooo=H20
P2Woool00`000?ooooooo`0Woooo=X20P0Koool30000B?ooo`B0P804coooo100001Soool60000
1Oooo`D0000=oooo100001_oool300001oooo`<0000>oooo100001goool3
000000Coool000000000000Koooo0`0001?oool40000ooooodCoool30000
4OooocF0P81Coooo=X20P0Koool30000B?ooo`B0P804coooo0`0000Soool300003_ooo`D0000Moooo0`0001Co
ool500005_ooo`<00009oooo100000koool500005oooo`@00009oooo0`00
00goool500006oooo`<00005oooo0`0000ooool500006oooo`@00002oooo
0`0001[oool300004oooo`D0003oooooA?ooo`<0000@oooo=H20P5?ooolf
P8201Oooo`<00019oooo1820P3G00003Oooo`<0000oooo0`00
01;oool60000=?ooo`<0000boooo3@0002[oool300002oooo`<0000`oooo
0`00037oool300001oooo`<0000Hoooo0`000?oooomMoooo0`0000oooole
P820DoooocJ0P804oooo0`0004[oool4P820=LcOooo`<00008oooo0`0000Woool30000
1_ooo`<00009oooo0`0000goool300004oooo`@0000doooo1@0003_oool3
0000:_ooo`@00009oooo100002koool3000000Coool000000000000^oooo
0`0000Woool300005oooo`<0003oooooG_ooo`@0000=oooo=H20P5?ooolf
P8200_ooo`@0001;oooo1820P3G00001ooooa000003oooo
200000Ooool800002Oooo`<0000Aoooo0`0000;oool300000000:oooo`l0000Zoooo200000?oool800009?ooo`P0
0007oooo200001?oool30000ooooofooooleP820DoooocJ0P81Aoooo1820
P5;Oooo`<00003oooo0`0007Koool300003Oooo`<0000:oooo
0`0002Woool300002Oooo`<0001Soooo0`0009Ooool30000oooooooooomo
oooo1820P5;
oooo200005Goool300004?ooo`<0000>oooo1P0002ooool300003oooo`<0
0003oooo0`0003Woool300000oooo`<0001foooo0`0000_oool700001_oo
o`L0000Toooo200000Goool80000GOooo`H0000ioooo2`0002koool;0000
6_ooo`<0003oooooooooogoooomJP820b?ooo`001oooo`P0000>oooo2000
05Goool300004?ooo`<0000>oooo1P0002ooool300003oooo`<00003oooo
0`0003Woool300000oooo`<0001foooo200000Koool700001_ooo`L0000T
oooo200000Goool80000GOooo`H0000ioooo2`0002koool;00005Oooo`P0
003oooooooooogoooomJP820b?ooo`007Oooo`P0001Eoooo0`00013oool3
00003_ooo`H0000_oooo0`000=3oool80000/?ooo`H0000ioooo2`0002ko
ool;00005Oooo`P0003oooooooooogoooomJP820b?ooo`00doooo`<0003@
oooo20000?oooom9oooo20000?ooooooooooOooooeZ0P838oooo003Coooo
0`000?oooooooooooooooooooonYooooFX20Poooo`/0000/oooo0P0004Soool<00004Oooo`P0000Toooo0P0003Go
ool800004?ooo`80002Foooo003ooooo=?oookR0P83oooooooooolGoool3
0000>oooo``0000[oooo0P0004Soool<00004Oooo`P0000Toooo0P0003Go
ool800004?ooo`80002Foooo003ooooo=?oookR0P83oooooooooolGoool3
0000A?ooo`@0000Zoooo0`0004goool300005?ooo`<0000Yoooo0`0003Wo
ool300004?ooo`<0002Eoooo003ooooo=?oookR0P83oooooooooolGoool3
0000AOooo`@0000Zoooo0`0004coool300005?ooo`<0000Zoooo0`0003So
ool300004Oooo`<0002Doooo003ooooo=?oookR0P83oooooooooolGoool3
0000A_ooo`<0000Zoooo0`0004goool300004oooo`<0000Zoooo0`0003So
ool300004Oooo`<0002Doooo003ooooo=?oookR0P83oooooooooolGoool3
0000A_ooo`<0000Zoooo100004coool300004oooo`<0000Zoooo100003Oo
ool300004Oooo`@0002Coooo003ooooo9?ooo`D0000;oooo^820P?oooooo
ooooD?oooa<00008oooo2@0000Koool700000oooo`D00003oooo2`0000?o
ool500000oooo`D00005oooo1P0000?oool600002_ooo`<0000Poooo1`00
00?oool500000oooo`D00007oooo1P0000;oool30000:oooo`<0000Moooo
1P0000?oool600000oooo`L00005oooo1`0000[oool400004_ooo`<0000:
oooo2@0000Koool900002Oooo`<0000Goooo4@0000ooool300004_ooo`<0
002Coooo003ooooo8_ooo`L0000;oooo^820P?ooooooooooD?oooa<00006
oooo3P0000?oool700000oooo`D00003oooo2`0000?oool500000oooo`D0
0003oooo2P000003oooo0000000000@0000:oooo0`00023oool700000ooo
o`D00003oooo1@0000Goool=0000:oooo`@0000Joooo2P000003oooo0000
000000@00003oooo1`0000Goool700002Oooo`D0000Boooo0`0000[oool9
00001_ooo`T00009oooo100001KooolC00003Oooo`<0000Boooo100009;o
ool00?oooolQoooo200000_oooleP820Olcoooo400002[oool300003?ooo`<0000;oooo0`000:Soool0
0?oooolNoooo0`0001?oooleP820Olcoooo0`000:Soool00?oooolNoooo0`0001?oooleP820Olc<
c0B0P83ooooooooooeCoool300003oooo`@00009oooo100000Goool30000
1Oooo`<00005oooo0`0000?oool300001Oooo`<00005oooo0`00013oool3
00003Oooo`<0000@oooo00<0003oooooool00oooo`030000oooooooo00Wo
ool300001Oooo`<00005oooo0`0000Coool400001oooo`D00009oooo00<0
003oooooool00oooo`030000oooooooo04;oool300002?ooo`@00008oooo
0`0000Koool300002_ooo`80000=oooo0`00013oool300001Oooo`<0000]
oooo3`0000koool30000Z?ooo`00oooooakoool300004oooocF0P81ocoooo0`00013oool00`000?ooooooo`03oooo00<0
003oooooool01ooooa@00006oooo4P0000Koool00`000?ooooooo`03oooo
00<0003oooooool0=_ooo`h00007oooo400000?oool800001oooo`P00009
oooo0`00017oool300000oooo`<0000^oooo0`0000[oool400003?ooo`<0
002Xoooo003ooooo7_ooo`<0000Coooo=H20P7oOooo`<00003oooo0`0007ooool80000
2_ooo`P0000^oooo3`0000coool80000Z?ooo`00oooooakoool300004ooo
ocF0P815c0P830P830P830P8300001Lc00001Ooo
o`h0000;oooo0P0000Ooool200002Oooo`l00007oooo3P0000[oool>0000
ooooooooooooooooVOooo`00H_ooofR0P81Coooo0`0001?oool9P8201000
01>0P80:00002h20P7o00002oooo`<00005oooo0`0000Woool?
00001oooo`l00007oooo4@000?oooooooooooooooiSoool006;ooomXP820
Doooo`<0000Coooo2H20P0@0000@P8202`0000f0P81ocP8202`0000n0P81ocoooo0`0000goool300002_ooo`<0
0005oooo0`000?ooooooooooooooojOoool006;ooomXP820Doooo`<0000C
oooo2H20P0@0000oooo0P0000[oool30000
1?ooo`<0000ooooo20000?ooooooooooooooof7oool006;ooomXP820Dooo
o`<0000Coooo1820P2d00004P820Olc0P80400000X20P0X00005P8202`0008n0P80Qoooo1@00
03Koool300002_ooo`<00009oooo0`00017oool300002Oooo`<00004oooo
100000_oool300002Oooo`@0000?oooo0P0000Coool300001?ooo`80000=
oooo0`0000koool500003_ooo`@0000;oooo0`0003Goool30000ooooo`Oo
oolhP820oooooooooolRoooo001RooooJ820P5?oool300004oooo`B0P802
00000h20P0h00005P8202`000960P80Qoooo1@0003Koool400002?ooo`@0
0009oooo0`00017oool400002?ooo`<00005oooo100000Woool400002Ooo
o`H00006oooo0P0000Coool300001Oooo`800004oooo0`0000coool30000
3_ooo`<00009oooo0P0000Koool400002Oooo`@0000eoooo0`000?ooool7
oooo>820P?oooooooooo8_ooo`00H_ooofR0P81Coooo0`0001?oool4P820
0P0000>0P80<00001H20P0/0000@P820Olcoooo100000Koool400001oooo`D00005oooo
1@0003Koool30000ooooo`OooolhP820hoooocJ0P83ooooo2?ooo`00H_oo
oa60P80X0000;h20P5?oool300004oooo`B0P80200000h20P0X00005P820
2`0001:0P81oc
00002?ooo`d00008oooo1P000003oooo0000000000T000000oooo`000000
000500001oooo`L00005oooo200000ooool=00002?ooo`d0000goooo0`00
0?ooool7oooo>820P>?ooolfP820ooooo`Soool006;ooolAP820:00002n0
P81Coooo0`0001?oool4P8200P0000>0P80800001820P0/0000EP820Olc<
c0B0P80Toooo4`0002Soool:00002?oooa400007oooo0`000003oooo0000
000000L0000:oooo2`0000Woool600000_ooo`T00002oooo1`0000Ooool7
00001Oooo`P0000@oooo300000Woool;0000>?ooo`<0003ooooo1oooocR0
P83Soooo=X20P?ooool8oooo001Roooo4H20P2P0000_P820Doooo`<0000C
oooo1820P0800003P8201P0000B0P80;00005h20P7o820P4_oool40000U?ooocJ0
P8001?ooo`00000000000?ooool4oooo001Roooo4H20P0@0000HP8202`00
00f0P80Gc0P80;00006h20P7o820P4[oool30000U_ooocJ0
P803oooo0`000?ooool2oooo001Roooo4H20P0@0000BP8202`0001>0P800
0lc820P4Woool30000
UoooocJ0P804oooo0`000?ooool1oooo001Roooo4H20P0@0000?P8202`00
01J0P803coooo1P0005[oool3
0000J?ooo`<0000Aoooo10000?7ooolhP820BOooo`<0002Goooo=X20P0Co
ool30000ooooo`7oool006;ooolAP820100000f0P80;00006820P0Coooo
3P0001Koool400005?ooo`B0P8060000:h20P7o820P4Soool30000V?ooocJ0P805oooo0`000?oo
ool006;oooloooo1@0001Ko
ool4P82000<00020P820P800;X20P7o00005Oooo`@0000E
oooo=H20P4Goo
oolAP8201LcP8204_ooo`<0000Woooo0`0001?oool@P820200000G0P80Coooo100002?oool400005?ooocJ0P808
oooo0`0000ooool80000iOooo`00H_ooofR0P81Coooo0`0001?oooleP820
4Lc820P4Goool300004ooo
o`B0P80200004X20P0L0000GP8205?ooo`<0000Soooo0`0001GooolfP820
2?ooo`<0000?oooo20000>Goool006;ooomXP820Doooo`<0000Coooo=H20
P17c820P4Goool300004oooo`B0P80200003H20P0L0000LP820
5Oooo`@0000Ooooo100001KooolfP8202?ooo`<0000Doooo0`000>Goool0
06;ooomXP820Doooo`<0000Coooo=H20P0cGoool006;ooomX
P820Doooo`<0000Coooo=H20P0cGoool006;ooomXP820Doooo`<0000Coooo=H20
P0coooo003ooooo7_ooo`<0000Coooo=H20P0cGoool00?oooolNoooo0`0001?oooleP8203oooo0`0001?ooolfP8207?ooo`<0000C
oooo0`0001gooolAP8202`0000J0P80600003X20P0Soool300005?ooo`<0
003Uoooo003ooooo7_ooo`<0000Coooo=H20P0c820P0koool500007oooo`D0
000>oooo0`0001?ooolfP8207?ooo`@0000Aoooo100001goool@P8203@00
00B0P80600003h20P0Soool300005?ooo`<0003Uoooo003ooooo7_ooo`<0
000Coooo=H20P0coooo003ooooo7_ooo`<0000Coooo=H20P4G0P808oooo0`0001Coool3
00004oooo`D0003=oooo003ooooo7_ooo`<0000Coooo=H20P4GGoool00?oooolNoooo0`0001?oooleP820ALcGoool00?oooolNoooo0`0001?oooleP820ALcGoool00?oooolNoooo0`0001?oooleP820ALc<
c0b0P807cP8201P0000Z0P808oooo0`0001Coool30000iOooo`00oooooakoool3
00004oooocF0P815c0P8040000
4820P0@0000;P8202?ooo`<0000Doooo0`000>Goool00?oooolNoooo0`00
01?oooleP820ALc820P4Goool300004oooo`n0P806cGoool00?oooolNoooo0`0001?oooleP820ALc820P4Goool300004oooo`n0P803c820P4Goool300004oooo`n0P8000lcP820
1oooo`<0003moooo003ooooo7_ooo`<0000Coooo^820P?ooooooooooG?oo
oa60P803c820P4Ooool30000VOooocJ0P806
oooo0`000?koool00?oooolNoooo0`000?ooool^oooo0`0002Woool30000
oooool[ooolhP820B?ooo`<0002Hoooo=X20P0Goool30000ooooo`00oooo
oakoool30000ooooobkoool30000:Oooo`<0003ooooob_ooocR0P818oooo
0`0009SooolfP8201Oooo`<0003ooooo003ooooo7_ooo`<0003ooooo;_oo
o`<0000Yoooo0`000?ooooo:oooo>820P4Soool30000V?ooocJ0P805oooo
0`000?ooool00?oooolNoooo0`000?ooool^oooo0`0002Woool30000oooo
ol[ooolhP820BOooo`<0002Goooo=X20P0Coool30000ooooo`7oool00?oo
oolNoooo0`0001Coool800001Oooo`L0003ooooo1_ooo`<0000Yoooo0`00
0?ooooo:oooo>820P4Woool30000UoooocJ0P804oooo0`000?ooool1oooo
003ooooo7_ooo`<0000Doooo200000Goool70000ooooo`Koool30000:Ooo
o`<0003ooooob_ooocR0P81:oooo0`0009KooolfP8200oooo`<0003ooooo
0_ooo`00oooooakoool300005?ooo`P00005oooo1`000<_oool00`000?oo
ooooo`0goooo0`0000_oool800001Oooo`L0000:oooo0`0001Woool>0000
4_ooo`l0003oooooP_ooocR0P81:oooo100009GooolfP8200_ooo`@0003o
oooo0_ooo`00oooooakoool300005_ooo`<0000:oooo0`000?ooo`<0000;oooo200000Goool700002_ooo`<0000Ioooo3P0001;oool?
0000oooooh;ooolhP820Boooo`<0002Eoooo=X20P0;oool30000ooooo`?o
ool00?oooolNoooo0`0001Ooool300002?ooo`<0003820P4_oool40000U?ooocJ0P8001?ooo`00000000000?ooool4
oooo003ooooo7_ooo`<0000Hoooo0`0000Koool30000c?oooa80000[oooo
0`0000goool300002_ooo`<0000oooo0`0000Soool300003Oooo`<0000V
oooo00<0003oooooool05_ooo`<0003oooooR?ooocR0P83Soooo=X20P?oo
ool8oooo003ooooo7_ooo`<0000Joooo0`0000;oool30000c?oooa@0000[
oooo0`0000ooool300001_ooo`<0000>oooo0`0002Coool300006?ooo`<0
003oooooR?ooocR0P83Soooo=X20P?ooool8oooo003ooooo7_ooo`<0000K
oooo1P000oooo`<0000@oooo0`0000Coool300003oooo`<0
000Roooo1@0001Soool30000ooooohSooolhP820hoooocJ0P83ooooo2?oo
o`00oooooakoool300007?ooo`@0003820
P?oooooooooo8_ooo`00oooooakoool300007?ooo`@0003?ooo`<0000Aoooo0`0001_oool0
0?oooooooooooooooooooooooooo2oooo`<0002Foooo0`0004goool30000
4oooo`<0000Xoooo0`0003Soool300004Oooo`<0000Koooo003ooooooooo
ooooooooooooooooo`_oool30000U_ooo`@000100003oooo`T00009oooo3P0000Soool?00001_ooo`L00005oooo
1`0000Coool?00003Oooo`L00009oooo3`0000coool600002_ooo`L00005
oooo1`0000[oool300008oooo`l00008oooo0P000003oooo0000000000H0
000@oooo1`0000koool50000:?ooo`<0000Moooo1P0000?oool600000ooo
o`L00005oooo1`0000[oool400004_ooo`<0000;oooo200000Goool70000
2_ooo`<0000Loooo2`00013oool300004_ooo`<0000Joooo003ooooooooo
oooooooooooo9Ooooa00000;oooo3P0000Koool>00002?ooo`l00006oooo
1`0000Goool700001?ooo`l000000003Oooo`/0
000;oooo1@0002Soool400006_ooo`X000000oooo`000000000400000ooo
o`L00005oooo1`0000Woool500004_ooo`<0000;oooo200000Goool70000
2_ooo`@0000Koooo2`00013oool300004_ooo`@0000Ioooo003ooooooooo
oooooooooooo9Ooooa400008oooo4@0000Goool>00002?ooo`l00006oooo
1`0000Goool700001?ooo`l0000;oooo3P0000Coool?00002?ooo`h00006
oooo1`0000Goool700002_ooo`<0000Soooo3`0000Ooool?00002oooo`h0
0008oooo0`000004oooo0000000000009oooo`D0000Hoooo4P0000?oool7
00001Oooo`L00009oooo1P00017oool300002oooo`P00005oooo1`0000[o
ool500006_ooo`/0000@oooo0`0001;oool500006?ooo`00oooooooooooo
ooooooooobOoool300002?ooo`D00006oooo1@0000Soool500002Oooo`<0
000Eoooo0`0000koool300002Oooo`<0000oooo1@0001goool3
00005?ooo`<0000Coooo1@0001Ooool00?oooooooooooooooooooolWoooo
0`0000_oool300001?ooo`<0000Ioooo0`0001Goool300003_ooo`<00009
oooo0`0000coool300004?ooo`<0000Foooo0`0000coool400002_ooo`@0
0006oooo0`0000Woool300003?ooo`<0000Yoooo0`0000koool200002_oo
o`<00009oooo0`0001?oool300000oooo`<00012oooo100000Woool30000
2?ooo`<00009oooo0`0000Woool300000oooo`<0000@oooo0`0000ooool3
00001_ooo`<0000aoooo0`0001Coool30000;oooo`00oooooooooooooooo
ooooobOoool300002oooo`@00003oooo4`0000Woool300005Oooo`<0000>
oooo0`0000Woool300003?ooo`<0000@oooo0`0001Koool300003?ooo`<0
000
oooo0`0000Woool300003?ooo`<0000@oooo0`0001Koool300003?ooo`<0
000oooo2`0000goool300004Ooo
o`<00007oooo0`0004Goool;00002?ooo`<00009oooo0`0000Ooool30000
1oooo`<0000>oooo0`0001?oool40000=Oooo`<0000Doooo0`0002ooool0
0?oooooooooooooooooooolWoooo0`0000coool300000oooo`@0000;oooo
0`0000[oool300005Oooo`<0000>oooo0`0000Woool300003?ooo`<0000@
oooo0`0001Koool300003Oooo`<0000:oooo0`0000Ooool300002Oooo`<0
000oooo1@0001?oool300004Oooo`<00007oooo0`0000_oool00`00
0?ooooooo`03oooo00<0003oooooool0>Oooo`<00008oooo0`0000Woool3
00001_ooo`<00009oooo0`0000goool300004oooo`@0000doooo1@0001?o
ool30000;oooo`00ooooooooooooooooooooobOoool300003?ooo`<00004
oooo100000Woool400002_ooo`<0000Eoooo0`0000koool400002?ooo`<0
000oooo1@0000Koool300003Oooo`<0000@oooo0`0001Koool30000
3_ooo`@00006oooo100000Soool500001_ooo`<0000=oooo0`00013oool0
0`000?ooooooo`03oooo00<0003oooooool04?ooo`<0000>oooo100000Ko
ool400002_ooo`<0000@oooo0`0000Woool300002_ooo`030000oooooooo
00?oool00`000?ooooooo`0hoooo100000Soool500001_ooo`<00006oooo
0`0000_oool300003?ooo`<0000Boooo1P0003;oool3000000Coool00000
0000000Boooo0`0002ooool00?oooooooooooooooooooolWoooo0`0000co
ool300001_ooo`d00008oooo3`0000Soool800003?oooa000008oooo2000
00coool@00002?ooo`P0000?oooo3@0000Koool@00003Oooo`<0000@oooo
00<0003oooooool00oooo`030000oooooooo00_oool800003oooo`d00006
oooo400000?oool900001Oooo`T00006oooo00<0003oooooool00oooo`03
0000oooooooo02goool>00001ooooa000003oooo200000Ooool800002Ooo
o`<0000Aoooo0`0000;oool30000_ooo`<0000Xoooo0`0000?oool3
0000M_ooo`<0000=oooo0`0000[oool30000:Oooo`<00009oooo0`0000ko
ool30000;oooo`00doooo`<0003ooooooooooooooom>oooo4@0002;oool4
0000Doooo`<0001Hoooo0`0000ooool300000oooo`<0000joooo0`0002So
ool300000oooo`<0001foooo0`0000_oool700001_ooo`L0000Toooo2000
00Goool800002oooo`<0000_oooo003Coooo0`000?ooooooooooooooodko
ool?00009Oooo`d0000:oooo0`0002Woool300004?ooo`<0000Foooo0`00
03ooool300003oooo`<00003oooo0`00017oool300009_ooo`<0000Xoooo
0`0000?oool30000M_ooo`<0000;oooo1`0000Koool700009?ooo`P00005
oooo200000_oool30000;oooo`00doooo`<0003ooooooooooooooom>oooo
3@0002Soool<00002_ooo`<0000Yoooo0`00013oool300005_ooo`<0000o
oooo0`0000ooool300000oooo`<0000Aoooo0`0002Koool30000:?ooo`<0
0003oooo0`0007Koool800001_ooo`L00006oooo1`0002Coool800001Ooo
o`P00006oooo200002ooool00=?oool30000ooooooooooooooooQOooo`T0
000;oooo0`0002Woool300004?ooo`<0000Foooo0`0003ooool30000:Ooo
o`<0000Voooo0`000:Ooool80000FOooo`P0000_oooo003Coooo0`000?oo
ooooooooooooooooooldoooo0`000?coool80000FOooo`P0000_oooo000d
oooo2P0009Goool30000Ioooo`X0001^oooo3000017oool800008?ooo`P0
003oooooooooooooool7oooo0`000?oooonEoooo000doooo2`0009Coool3
0000Ioooo`/0000Soooo0P0004Soool<00004Oooo`P0000Poooo2000013o
ool20000ooooooooooodoooo0`000?oooonEoooo000doooo300009?oool3
0000Ioooo``0000Roooo0P0004Soool<00004Oooo`P0000Poooo2000013o
ool20000ooooooooooodoooo0`000?oooonEoooo000moooo100009;oool3
0000L?ooo`@0000Qoooo0`0004goool300005?ooo`<0000Zoooo0`00013o
ool30000ooooooooooocoooo0`000?oooonEoooo000noooo1000097oool3
0000LOooo`@0000Qoooo0`0004coool300005?ooo`<0000Zoooo0`00017o
ool30000oooooooooooboooo0`000?oooonEoooo000ooooo0`00097oool3
0000L_ooo`<0000Qoooo0`0004goool300004oooo`<0000Zoooo0`00017o
ool30000oooooooooooboooo20000?oooon@oooo000ooooo0`00097oool3
0000L_ooo`<0000Qoooo100004coool300004oooo`<0000Zoooo0`00017o
ool40000oooooooooooaoooo20000?oooon@oooo0002oooo2@0000Koool9
00000_ooo`l000000003Oooo`/00003oooo1`0000?oool5
00000oooo`D00005oooo3@0002;oool400006_ooo`X000000oooo`000000
000400000oooo`L00005oooo1`0000Woool500004_ooo`<0000;oooo2000
00Goool700002oooo`<0000Boooo10000?oooooooooooooooooooon9oooo
0002oooo2@0000Koool900000_ooo`l00008oooo3`0000Ooool>00001_oo
o`h00009oooo3`0000_oool>00000oooo`L00005oooo1`000003oooo0000
000000D00003oooo1@0000?oool500002Oooo`<0000Soooo3`0000_oool>
000000?oool0000000001@0000?oool500000oooo`D00003oooo3`0002;o
ool500006?oooa800003oooo1`0000Goool700002Oooo`H0000Aoooo0`00
00_oool800001Oooo`L0000;oooo0`0001;oool50000oooooooooooooooo
ooooohSoool000Goool300003?ooo`<0000;oooo0`0000goool500001Ooo
o`H00006oooo1@0000Koool500002Oooo`<0000Foooo0`00013oool40000
1_ooo`D00005oooo0`0000Woool300001Oooo`<00005oooo0`0000Goool3
00002oooo`<0000Soooo1@0000Ooool400002Oooo`@00006oooo1@0000?o
ool300001Oooo`<00005oooo0`0000Coool500001Oooo`H0000Soooo1000
01Ooool400001_ooo`H00008oooo0`0000Woool300002_ooo`<000001?oo
o`0000000000017oool300003Oooo`<0000:oooo0`0000goool300004ooo
o`@0003oooooooooooooooooooooR?ooo`001Oooo`<0000oooo0`0000Soool30000
3_ooo`<0000Coooo1@000?oooooooooooooooooooon7oooo0006oooo0`00
00[oool300003?ooo`<000000003Oooo`<000000003Oooo`<0000Oooo`<00008oooo1000
00Soool300001_ooo`<0000:oooo0P0000goool300004oooo`@0000Coooo
0`000?oooooooooooooooooooonOoooo0009oooo0`0000Coool300003ooo
o`<0000=oooo1@0000Goool600001oooo`@00006oooo100000[oool80000
0oooo`@0000:oooo0`00013oool300004Oooo`H00005oooo0`0000Koool4
00001?ooo`@00004oooo0`0000_oool300004?ooo`030000oooooooo00?o
ool00`000?ooooooo`0;oooo100000Koool400002_ooo`<0000?oooo1000
00Coool400001?ooo`<00004oooo1@0000Goool600002Oooo`030000oooo
oooo00?oool00`000?ooooooo`0hoooo100000Soool500001_ooo`<00006
oooo0`0000_oool300003?ooo`<0000Boooo1P0001;oool30000oooooooo
oooooooooooooiooool000Woool300000oooo`<0000@oooo0`0000kooolB
00001Oooo`d00007oooo1P000003oooo0000000000T00005oooo200000co
ool@00002?ooo`h00004oooo500000coool300004?ooo`030000oooooooo
00?oool00`000?ooooooo`0oooo0`00
0?oooooooooooooooooooonOoooo000;oooo1@0001;oool30000J?ooo`<0
000Aoooo0`0002ooool300003oooo`<00003oooo0`0002Coool30000?_oo
o`<00003oooo0`0007Koool300003Oooo`<0000:oooo0`0000goool30000
oooooooooooooooooooooiooool000Ooool900004_ooo`<0001Xoooo0`00
017oool30000;oooo`<0000?oooo0`0000?oool300009?ooo`<0000noooo
0`0000?oool30000M_ooo`<0000;oooo1`0000Koool700002oooo`<0003o
ooooooooooooooooooooWoooo`001oooo`P0000>oooo200005Goool30000
4?ooo`<0000>oooo1P0002ooool300003oooo`<00003oooo0`0002Coool3
0000?_ooo`<00003oooo0`0007Koool300002oooo`L00006oooo1`0000_o
ool30000oooooooooooooooooooooiooool000Ooool800003_ooo`P0001E
oooo0`00013oool300003_ooo`H0000_oooo0`0000ooool300000oooo`<0
000Toooo0`0003koool300000oooo`<0001foooo200000Koool700001_oo
o`L00006oooo20000?oooooooooooooooooooonOoooo000Moooo200005Go
ool300004?ooo`<0000>oooo1P0002ooool30000??ooo`<0002moooo2000
023oool80000oooooooooooooooooooooiooool00=?oool30000o?ooo`P0
000Poooo20000?oooooooooooooooooooonOoooo003Coooo0`000?oooooo
ooooooooooooooooooooc?ooo`00doooo`<0003ooooooooooooooooooooo
ooooolcoool00=?oool30000ooooooooooooooooooooooooooo"], "Input",
CellMargins->{{36.3125, Inherited}, {Inherited, Inherited}},
Evaluatable->False,
TextAlignment->Left,
TextJustification->1,
ImageSize->{429, 211.25},
ImageMargins->{{0, 0}, {0, 0}},
ImageRegion->{{0, 1}, {0, 1}},
CellTags->{"EPS", "FileName->withLGS.eps"}]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell["Computing (Within Predicate Logic)", "Section"],
Cell[CellGroupData[{
Cell["Programs are Predicate Logic Formulae", "Subsection"],
Cell[BoxData[
RowBox[{
StyleBox["Definition",
FontWeight->"Bold"], "[",
RowBox[{
"\"\\"", ",", \(any[m, n]\), ",", "\n", "\t", GridBox[{
{\(m + 0 = m\), "\"\< +0:\>\""},
{\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), "\"\< + .:\>\""}
},
ColumnAlignments->{Left}]}], "]"}]], "Input",
CellTags->"Definition (addition)"],
Cell[CellGroupData[{
Cell[BoxData[
\(Definition["\"] // InputForm\)], "Input"],
Cell["\<\
\[Bullet]def[\"addition\", \[Bullet]range[\[Bullet]simpleRange[
\[Bullet]var[m]], \[Bullet]simpleRange[\[Bullet]var[n]]], True,
\[Bullet]flist[\[Bullet]lf[\" +0:\", \[Trademark]Equal[\[Trademark]Plus[\
\[Bullet]var[m],
0], \[Bullet]var[m]]], \[Bullet]lf[\" + .:\",
\[Trademark]Equal[\[Trademark]Plus[\[Bullet]var[m], \[Trademark]SuperPlus[
\[Bullet]var[n]]], \
\[Trademark]SuperPlus[\[Trademark]Plus[\[Bullet]var[m],
\[Bullet]var[n]]]]]]]\
\>", "Output"]
}, Open ]],
Cell[CellGroupData[{
Cell[BoxData[
\(Compute[\(\(\(0\^+\)\^+\)\^+\) + \(\(0\^+\)\^+\),
using \[Rule] Definition["\"]]\)], "Input"],
Cell[BoxData[
\(\(\((\(\((\(\((\(\((\(0\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\)\)], \
"Output"]
}, Open ]],
Cell[CellGroupData[{
Cell[BoxData[
\(Compute[\(\(\(0\^+\)\^+\)\^+\) + \(\(0\^+\)\^+\),
using \[Rule] \[LeftAngleBracket]\[RightAngleBracket]]\)], "Input"],
Cell[BoxData[
\(\(\((\(\((\(0\^+\))\)\^+\))\)\^+\) + \(\((\(0\^+\))\)\^+\)\)], "Output"]
}, Open ]],
Cell[BoxData[
RowBox[{
StyleBox["Definition",
FontWeight->"Bold"], "[",
RowBox[{
"\"\\"", ",", \(any[m, n]\), ",", "\n", "\t",
GridBox[{
{\(m*0 = 0\), "\"\< *0:\>\""},
{\(m*\(n\^+\) = \((m*n)\) + m\), "\"\< * .:\>\""}
},
ColumnAlignments->{Left}]}], "]"}]], "Input",
CellTags->"Definition (multiplication)"],
Cell[CellGroupData[{
Cell[BoxData[
\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(0\^+\)\^+\),
using \[Rule] Definition["\"]]\)], "Input"],
Cell[BoxData[
\(\(\((\(\((\(0\^+\))\)\^+\))\)\^+\)*\(\((\(0\^+\))\)\^+\)\)], "Output"]
}, Open ]],
Cell["No hidden knowledge is used!", "Text"],
Cell[CellGroupData[{
Cell[BoxData[
\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\),
using \[Rule] \[LeftAngleBracket]Definition["\"],
Definition["\"]\[RightAngleBracket]]\)], "Input"],
Cell[BoxData[
\(\(\((\(\((\(\((\(\((\(\((\(\((\(\((\(\((\(\((\(\((\(\((\(0\^+\))\)\^+\))\
\)\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\))\)\^+\
\)\)], "Output"]
}, Open ]],
Cell[CellGroupData[{
Cell[BoxData[
\(Compute[\(\(\(0\^+\)\^+\)\^+\)*\(\(\(\(0\^+\)\^+\)\^+\)\^+\),
using \[Rule] \[LeftAngleBracket]Definition["\"]\
\[RightAngleBracket]]\)], "Input"],
Cell[BoxData[
\(\((\((\((0 + \(\((\(\((\(0\^+\))\)\^+\))\)\^+\))\) + \
\(\((\(\((\(0\^+\))\)\^+\))\)\^+\))\) + \(\((\(\((\(0\^+\))\)\^+\))\)\^+\))\) \
+ \(\((\(\((\(0\^+\))\)\^+\))\)\^+\)\)], "Output"]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell["Tracing Computations", "Subsection"],
Cell["See proving.", "SmallText"]
}, Open ]],
Cell[CellGroupData[{
Cell["Using the Theory Construct", "Subsection"],
Cell[BoxData[
RowBox[{"Theory", "[",
RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{
{\(Definition["\"]\)},
{\(Definition["\