mod Ex04 logic: 'cl'

rem 
  \para \bf  5. CVIČENIE Z PREDMETU LOGIKA PRE INFORMATIKOV 2  \end 
  \para* http://ii.fmph.uniba.sk/cl/courses/lpi2/ex/ex05.cl 

rem 
  \para* \it  Dátum:  \end štvrtok 28. 10. 2004 
  \para* \it  Odporúčaná verzia CL:  \end 5.81.16 
  \para* \it  WWW stránka predmetu:  \end 
  http://ii.fmph.uniba.sk/cl/courses/lpi2?lang=sk 
  \para* \it  Kontakt na cvičiaceho:  \end mailto:kluka@fmph.uniba.sk 

rem 
  \para Preskočte nasledujúce komponenty až po nadpis "Peanova aritmetika". 

appldisp/2 Plus_d
  Infix(Arg(0),40,1,Op(Ent('dotplus'),0),Arg(1))

appldisp/2 Plus_na_d
  Infix(Arg(0),40,0,Op(Ent('dotplus'),0),Arg(1))

appldisp/2 Times_na_d
  Infix(Arg(0),45,0,Op(Ent('bull'),0),Arg(1))

appldisp/2 Times_d
  Infix(Arg(0),45,1,Op(Ent('bull'),0),Arg(1))

appldisp/1 Phi_d
  Prefix(70,2,Id(5,'A',0),Fenced(Op('[',0),Arg(0),Op(']',0)))

appldisp/2 Phi2_d
  Prefix(90,2,Id(5,'A',0),
         Fenced(Op('[',0),Infix(Arg(0),30,2,Op(';',0),Arg(1)),Op(']',0)))

appldisp/1 S_d
  Std('S',0)

appldisp/5 Rule4
  Frac(Infix(Arg(0),1,3,Id(0,' ',0),
             Infix(Arg(1),1,3,Id(0,' ',0),Infix(Arg(2),1,3,Id(0,' ',0),Arg(3)))),1,
       Arg(4))

appldisp/2 Eq
  Infix(Arg(0),25,0,Op('=',0),Arg(1))

appldisp/0 Tau
  Id(0,Ent('tau'),0)

appldisp/0 Tau1
  Subsup(Id(0,Ent('tau'),0),75,Num('1',0),None)

appldisp/0 Taun
  Subsup(Id(0,Ent('tau'),0),75,Id(1,'n',0),None)

appldisp/0 Rho
  Id(0,Ent('rho'),0)

appldisp/0 Rho1
  Subsup(Id(0,Ent('rho'),0),75,Num('1',0),None)

appldisp/0 Rhon
  Subsup(Id(0,Ent('rho'),0),75,Id(1,'n',0),None)

appldisp/0 Ldots
  Op(Ent('hellip'),0)

appldisp/1 Goal
  Postfix(Arg(0),4,1,Op(Ent('lowast'),0))

appldisp/3 B_d
  Prefix(90,2,Id(5,'B',0),
         Fenced(Op('[',0),
                Infix(Arg(0),30,2,Op(',',0),Infix(Arg(1),30,2,Op(',',0),Arg(2))),
                Op(']',0)))

appldisp/2 Impl
  Infix(Arg(0),10,2,Op(Ent('rarr'),0),Arg(1))

appldisp/2 Forall
  Prefix(20,2,Prefix(20,2,Op(Ent('forall'),0),Arg(0)),Arg(1))

appldisp/3 Split_rule2
  Frac(Arg(0),1,Infix(Arg(1),1,3,Op(Ent('mid'),0),Arg(2)))

rem 
  \para \bf  PEANOVA ARITMETIKA  \end 

rem 
  \para \it  Peanova aritmetika  \end je teória v logike prvého rádu (teda 
  kvantifikačnej logike), ktorá formalizuje prirodzené čísla a operácie na 
  nich. Jazyk Peanovej aritmetiky tvoria funkčné symboly pre konštantu 
  \ft 0 \end, unárnu funkciu \it  nasledovník  \end (successor) \ft S(x) \end, 
  binárnu funkciu \it  sčítanie  \end (addition) \ft x+y \end a binárnu 
  funkciu \it  násobenie  \end (multiplication) \ft x*y \end. 
  \para \it  Axiómy Peanovej aritmetiky  \end sa skladajú zo šiestich axióm 
  \ft Q1 \end až \ft Q6 \end (viď nižšie) opisujúcich vlastnosti nuly, 
  nasledovníka, sčítania a násobenia a z nekonečne veľa axióm 
  zodpovedajúcich \it  schéme axióm indukcie  \end: 
  \eq* 
    Phi_d(0) & \a x(Phi_d(x) -> Phi_d S(x)) -> Phi_d(x)
  \end
  \para* v ktorej \ft Phi_d(x) \end zastupuje ľubovoľnú formulu s nejakou 
  voľnou premennou, ktorú sme označili \ft x \end. Formule \ft Phi_d(x) \end 
  v tomto kontexte hovoríme \it  indukčná formula  \end ( \it  induction 
  formula  \end) a premennej \ft x \end hovoríme \it  indukčná premenná 
   \end ( \it  induction variable  \end). Formula \ft Phi_d(0) \end sa nazýva 
  \it  bázou indukcie  \end ( \it  base case  \end), formula 
  \ft \a x(Phi_d(x) -> Phi_d S(x)) \end sa nazýva \it  indukčným krokom  \end 
  ( \it  inductive case  \end). V dôkaze indukčného kroku sa 
  \ft Phi_d(x) \end nazýva \it  indukčným predpokladom  \end ( \it  inductive 
  hypothesis  \end, IH). Ak má formula \ft Phi_d(x) \end ďalšie voľné 
  premenné, nazývame ich \it  parametrami  \end. 
  \para Upozorňujeme, že odteraz sú všetky voľné premenné axióm a 
  teorém \bf  implicitne všeobecne kvantifikované  \end. Napríklad axiómu 
  \ft Q2 \end: \ft S(x) = S(y) -> x = y \end chápeme ako 
  \ft \a x\a y(S(x) = S(y) -> x = y) \end. Túto formulu nazývame \it  
  všeobecným uzáverom  \end ( \it  universal closure  \end) formuly 
  \ft S(x) = S(y) -> x = y \end. 

rem 
  \para \bf  Cvičenie 1.  \end \header* fun/2 Add  \end 
  \header* fun/2 Mul  \end Dokážte v teórii \ft Peano \end, že tvrdenia 
  \ft T1 \end až \ft T4 \end (niektoré základné vlastnosti sčítania) sú 
  logickými dôsledkami axióm Peanovej aritmetiky. Pre každé z týchto 
  tvrdení musíte objaviť \bf  potrebnú indukčnú axiómu  \end (teda 
  inštanciu schémy axióm indukcie), ktorú vložíte bezprostredne pred 
  dokazované tvrdenie. Ako príklad sme uviedli indukčnú axiómu \ft Ia0 \end 
  a dôkaz tvrdenia \ft T0 \end. 
  \para Neformálne návody k dôkazom týchto cvičení nájdete v článku 
  \it  7.1 Basic Theorems in PA  \end textu \it  Metamathematics of Computer 
  Programming  \end prístupného cez webstránku predmetu LPI2 (priamu linku 
  http://ii.fmph.uniba.sk/cl/courses/lpi2/lect/meta.pdf#section.7.1 odporúčame 
  otvoriť v novej záložke Mozilly ( Ctrl-T )). 

theory Peano logic: 'fol_def'

rem 
  \para \header* fun/2 Add  \end \header* fun/2 Mul  \end Funkčným symbolom 
  pre nasledovníka je \ft S_d(x) \end zobrazovaný ako \ft S(x) \end. V rámci 
  tohto a nasledujúceho cvičenia označujeme sčítanie funkčným symbolom 
  \ft Add(x,y) \end, zobrazovaným ako \ft Plus_d(x,y) \end. Vo všetkých 
  cvičeniach označujeme násobenie funkčným symbolom \ft Mul(x,y) \end, 
  zobrazovaným ako \ft Times_d(x,y) \end. 

fun/2 Add 'Plus_na_d'

fun/2 Mul 'Times_na_d'

axiom Q1
  0 != S(x)

axiom Q2
  S(x) = S(y) -> x = y

axiom Q3
  Add(0,y) = y

axiom Q4
  Add(S(x),y) = S Add(x,y)

axiom Q5
  Mul(0,y) = 0

axiom Q6
  Mul(S(x),y) = Add(Mul(x,y),y)

rem 
  \para Sľúbený príklad: Axióma indukcie \ft Ia0 \end potrebná na dôkaz 
  tvrdenia \ft T0 \end. Formulou \ft Phi_d(x) \end je v tomto prípade priamo 
  dokazované tvrdenie, teda \ft Add(x,0) = x \end. \ft Phi_d(0) \end je 
  \ft Add(0,0) = 0 \end a \ft Phi_d S(x) \end je \ft Add(S(x),0) = S(x) \end. 

axiom Ia0
  Add(0,0) = 0 & \a x(Add(x,0) = x -> Add(S(x),0) = S(x)) -> Add(x,0) = x

thm T0
  Add(x,0) = x
proof 
 use Ia0.0; x
  split Add(0,0) = 0 & \a x(Add(x,0) = x -> Add(S(x),0) = S(x)) -> Add(x,0) = x.2,
                                                                                (4,
                                                                                 1,
                                                                                 1,
                                                                                 0),
                                                                                0
   weak* Add(x,0) = x
    use Q3; 0 proved..
   weak* Add(x,0) = x
    eigen* \a x(Add(x,0) = x -> Add(S(x),0) = S(x)).0; y
     use Q4; y; 0 proved...
   proved...

rem 
  \para Komentár k dôkazu \ft T0 \end: Po použití indukčnej axiómy na ňu 
  okamžite aplikujeme pravidlo split. Dôkaz sa rozvetví a posledná vetva sa 
  ihneď uzavrie. Zo zostávajúcich vetiev (bázy indukcie a indukčného 
  kroku) je dobré odstrániť pôvodný cieľ \ft Add(x,0) = x \end, aby nás 
  pri dôkaze nemiatol. Urobíme to príkazom \bf  weak*  \end. V niektorých 
  dôkazoch môže byť podobne výhodné zbaviť sa už nepotrebných 
  predpokladov príkazom \bf  weak  \end. 
  \para Báza indukcie je jednoduchým dôsledkom axiómy \ft Q3 \end. Odvodíme 
  ho použitím tejto axiómy a aplikáciou inštanciačného pravidla (CL 
  umožňuje urobiť tieto dva kroky jediným príkazom \bf  use  \end). 
  \para V indukčnom kroku po použití axiómy \ft Q4 \end dokazovač CL ihneď 
  uzavrel dôkaz. Stalo sa tak preto, že dokazovač \bf  automaticky používa 
  tablové ekvačné pravidlá  \end. Podrobný postup je takýto: 
  \para Podľa axiómy \ft Q4 \end platí \ft Add(S(y),0) = S Add(y,0) \end. Z 
  indukčného predpokladu \ft Add(y,0) = y \end pravidlom substitúcie pre 
  funkciu \ft S \end odvodíme \ft S Add(y,0) = S(y) \end a pravidlom 
  tranzitívnosti dostávame \ft Add(S(y),0) = S(y) \end, čo je presne náš 
  cieľ. 

rem 
  \para Tvrdeniu \ft T1 \end hovoríme \it  analýza prípadov nula a kladné 
  číslo  \end ( \it  case analysis on 0 and on positive numbers  \end) a je 
  trocha netypické: Na jeho dôkaz je potrebná indukcia, ale v indukčnom 
  kroku vôbec nepoužijeme indukčný predpoklad. Všimnite si, ako dokazovač 
  automaticky použije pravidlo reflexivity a pravidlo substitúcie pre funkciu 
  \ft S \end. 

axiom Ax1
  (0 = 0 \/ \e y 0 = S(y)) & 
  \a x(x = 0 \/ \e y x = S(y) -> S(x) = 0 \/ \e y S(x) = S(y)) -> 
  x = 0 \/ \e y x = S(y)

thm T1
  x = 0 \/ \e y x = S(y)
proof 
 use Ax1.0:0; x
  split \a x(x = 0 \/ \e y x = S(y) -> S(x) = 0 \/ \e y S(x) = S(y)) -> 
        x = 0 \/ \e y x = S(y).2,1,0
   eigen* \a x(x = 0 \/ \e y x = S(y) -> S(x) = 0 \/ \e y S(x) = S(y)).0:0; z
    inst* \e y S(z) = S(y); z proved..
   split x = 0 \/ \e y x = S(y).4,0,0,0
    proved
    proved....

rem 
  \para Pri dôkaze nasledujúceho tvrdenia \ft T2 \end (pre ktoré za 
  zaužíval neformálny názov "čiarková lema") si už v báze indukcie 
  pravdepodobne všimnete, že dokazovač CL používa viac, ako len ekvačné 
  pravidlá, lebo po použití axióm sčítania zmení cieľ. 
  \para To je možné na základe \it  Leibnitzovho pravidla  \end: 
  \eq* 
    Rule4(Eq(Tau1,Rho1),Ldots,Eq(Taun,Rhon),B_d(Tau1,Ldots,Taun),
          B_d(Rho1,Ldots,Rhon))
  \end
  \para ktoré možno jednou vetou zhrnúť ako \it  rovné možno nahradiť 
  rovným  \end. Leibnitzovo pravidlo je odvodené, teda každý dôkaz, ktorý 
  ho používa sa dá pretransformovať na dôkaz, ktorý namiesto neho 
  používa iba základné ekvačné a propozičné pravidlá (viď 
  Meta-Mathematics... odsek 6.1.2). Potom sa ľahko sa dá odvodiť aj 
  Leibnitzovo pravidlo pre ciele: 
  \eq* 
    Rule4(Eq(Tau1,Rho1),Ldots,Eq(Taun,Rhon),Goal B_d(Tau1,Ldots,Taun),
          Goal B_d(Rho1,Ldots,Rhon))
  \end
  \para Ak sa v dôkaze vyskytne predpoklad \ft Tau = Rho \end, dokazovač \bf  
  automaticky zamení \ft Tau \end za \ft Rho \end  \end vo všetkých 
  nasledujúcich predpokladoch a vo všetkých cieľoch. Táto zámena má 
  často za následok prekvapujúce ukončenie dôkazu. Niekedy sa formuly po 
  aplikovaní takejto zámeny veľmi zneprehľadnia. Vtedy môže pomôcť 
  explicitné použitie pravidla symetrie príkazom \bf  sym  \end 
  \ft Tau = Rho \end, ktoré predpoklad \ft Tau = Rho \end "obráti" na 
  \ft Rho = Tau \end. 

axiom Ax2
  Add(S(0),y) = Add(0,S(y)) & 
  \a x(Add(S(x),y) = Add(x,S(y)) -> Add(S S(x),y) = Add(S(x),S(y))) -> 
  Add(S(x),y) = Add(x,S(y))

thm T2
  Add(S(x),y) = Add(x,S(y))
proof 
 use Ax2.0; y; x
  split Add(S(0),y) = Add(0,S(y)) & 
        \a x(Add(S(x),y) = Add(x,S(y)) -> Add(S S(x),y) = Add(S(x),S(y))) -> 
        Add(S(x),y) = Add(x,S(y)).2,1,0
   split* Add(S(0),y) = Add(0,S(y)) & 
          \a x(Add(S(x),y) = Add(x,S(y)) -> Add(S S(x),y) = Add(S(x),S(y))).4,0,
                                                                            0,0
    use Q3; S(y)
     use Q3; y
      use Q4; 0; y proved...
    weak* Add(S(x),y) = Add(x,S(y))
     eigen* \a x(Add(S(x),y) = Add(x,S(y)) -> Add(S S(x),y) = Add(S(x),S(y))).0; z
      use Q4; z; S(y)
       use Q4; S(z); y proved.....
   proved...

axiom Lema1ax
  Add(0,0) = 0 & \a x(Add(x,0) = x -> Add(S(x),0) = S(x)) -> Add(x,0) = x

lemma Lema1
  Add(x,0) = x
proof 
 use Lema1ax.0; x
  split Add(0,0) = 0 & \a x(Add(x,0) = x -> Add(S(x),0) = S(x)) -> Add(x,0) = x.2,
                                                                                1,
                                                                                0
   weak* Add(x,0) = x
    split* Add(0,0) = 0 & \a x(Add(x,0) = x -> Add(S(x),0) = S(x)).4,0,0,0
     use Q3; 0 proved.
     eigen* \a x(Add(x,0) = x -> Add(S(x),0) = S(x)).0; y
      use Q4; y; 0 proved....
   proved...

axiom Ax3
  Add(0,y) = Add(y,0) & \a x(Add(x,y) = Add(y,x) -> Add(S(x),y) = Add(y,S(x))) -> 
  Add(x,y) = Add(y,x)

thm T3
  Add(x,y) = Add(y,x)
proof 
 use Ax3.0; y; x
  split Add(0,y) = Add(y,0) & 
        \a x(Add(x,y) = Add(y,x) -> Add(S(x),y) = Add(y,S(x))) -> 
        Add(x,y) = Add(y,x).2,1,0
   weak* Add(x,y) = Add(y,x)
    split* Add(0,y) = Add(y,0) & 
           \a x(Add(x,y) = Add(y,x) -> Add(S(x),y) = Add(y,S(x))).4,0,0,0
     use Q3; y
      use Lema1; y proved..
     eigen* \a x(Add(x,y) = Add(y,x) -> Add(S(x),y) = Add(y,S(x))).0; z
      use Q4; z; y
       use Q4; y; z
        use T2; y; z proved......
   proved...

axiom Ax4
  Add(Add(0,y),z) = Add(0,Add(y,z)) & 
  \a x(Add(Add(x,y),z) = Add(x,Add(y,z)) -> 
       Add(Add(S(x),y),z) = Add(S(x),Add(y,z))) -> 
  Add(Add(x,y),z) = Add(x,Add(y,z))

thm T4
  Add(Add(x,y),z) = Add(x,Add(y,z))
proof 
 use Ax4.0; y; z; x
  split Add(Add(0,y),z) = Add(0,Add(y,z)) & 
        \a x(Add(Add(x,y),z) = Add(x,Add(y,z)) -> 
             Add(Add(S(x),y),z) = Add(S(x),Add(y,z))) -> 
        Add(Add(x,y),z) = Add(x,Add(y,z)).2,1,0
   weak* Add(Add(x,y),z) = Add(x,Add(y,z))
    split* Add(Add(0,y),z) = Add(0,Add(y,z)) & 
           \a x(Add(Add(x,y),z) = Add(x,Add(y,z)) -> 
                Add(Add(S(x),y),z) = Add(S(x),Add(y,z))).4,0,0,0
     use Q3; y
      use Q3; Add(y,z) proved..
     eigen* \a x(Add(Add(x,y),z) = Add(x,Add(y,z)) -> 
                 Add(Add(S(x),y),z) = Add(S(x),Add(y,z))).0; xx
      use Q4; xx; y
       use Q4; Add(xx,y); z
        use Q4; xx; Add(y,z) proved......
   proved...

end theory Peano

rem 
  \para \bf  Cvičenie 2.  \end Dokážte nasledujúce tvrdenia \ft T3 \end, 
  \ft T4 \end, \ft T5 \end, \ft T6 \end, \ft T7 \end v Peanovej aritmetike 
  pomocou \bf  pravidla  \end matematickej indukcie: 
  \eq* 
    Split_rule2(Goal Phi_d(x),Goal Phi_d(0),Goal Impl(Phi_d(x),Phi_d S(x)))
  \end
  \para V CL použijeme toto pravidlo príkazom \bf  ind  \end \ft N1 \end; 
  \ft x \end. 
  \para Tvrdenia \ft T0 \end, \ft T1 \end, \ft T2 \end ste dokázali v 
  predošlom cvičení. Aby ste ich nemuseli dokazovať znova, dodali sme ich do 
  teórie \ft Peano_cldef \end ako axiómy. V tejto teórii je dokazovač CL 
  nastavený tak, aby okrem automatických odvodení z predošlého cvičenia 
  \bf  automaticky  \end používal 
  \items 
   \item \para axiómy nasledovníka \ft Q1 \end a \ft Q2 \end (sú 
         zabudované); 
   \item \para axiómy sčítania \ft Q3 \end a \ft Q4 \end (automaticky sa 
         používajú vďaka klauzálnej definícii \ft Plus_d(x,y) \end 
         uvedenej na začiatku teórie; klauzálnu definíciu sme mohli použiť 
         preto, že obe klauzuly sú dokázateľné v Peanovej aritmetike, v 
         tomto prípade sú dokonca jej axiómami). 
  \end

theory Peano_cldef logic: 'cl'

fun/2 Add 'Plus_na_d'
  Add(0,y) = y
  Add(S(x),y) = S Add(x,y)

axiom T0
  Add(x,0) = x

axiom T1
  x = 0 \/ \e y x = S(y)

axiom T2
  Add(S(x),y) = Add(x,S(y))

rem 
  \para Komutatívnosť sčítania ( \ft T3 \end) ste dokázali už v predošlom 
  cvičení. Uvádzame ju aj v tomto, aby ste mohli porovnať, ako sa zmení 
  dôkaz vďaka pravidlu indukcie a automatickému používaniu axióm 
  nasledovníka a sčítania. 

thm T3
  Add(x,y) = Add(y,x)
proof 
 ind N1; x @ 0; x
  use T0; y proved.
  use T2; y; x proved...

rem 
  \para Asociatívnosť sčítania ( \ft T4 \end) ukazuje, že niektoré dôkazy 
  sa stanú úplne triviálnymi. 

thm T4
  Add(Add(x,y),z) = Add(x,Add(y,z))
proof 
 ind N1; x @ 0; x
  proved
  proved..

rem 
  \para V \ft T5 \end je implikácia \ft x = 0 -> Add(x,y) = y \end triviálna. 
  Obrátenú implikáciu dokážte indukciou. 

thm T5
  Add(x,y) = y <-> x = 0
proof 
 split* Add(x,y) = y <-> x = 0.2,0,0
  ind N1; y @ 0; y
   use T0; x proved.
   split Add(x,y) = y -> x = 0.2,1,0
    use T2; x; y proved.
    proved..
  proved..

thm T6
  Add(z,x) = Add(z,y) -> x = y
proof 
 ind N1; z @ 0; z
  proved
  proved..

thm T7
  Add(x,z) = Add(y,z) -> x = y
proof 
 use T3; x; z
  use T3; y; z
   use T6; z; x; y proved....

end theory Peano_cldef

rem 
  \para \bf  Cvičenie 3.  \end Dokážte v Peanovej aritmetike nasledujúce 
  vlastnosti násobenia. Podobne ako v predošlom cvičení používajte 
  pravidlo indukcie, nie axiómy indukcie. 
  \para V tomto cvičení používame sčítanie \ft x+y \end zabudované do CL 
  zapisované ako infixový operátor +. Dokazovač pozná všetky vlastnosti 
  sčítania, ktoré ste dokázali v predošlých cvičeniach, okrem analýzy 
  prípadov \ft T1 \end. Na analýzu prípadov 0 a kladné číslo na term 
  \ft Tau \end však môžete použiť príkaz \bf  case  \end \ft N1 \end; 
  \ft Tau \end. 
  \para Násobenie sme zadefinovali klauzálne, teda axiómy \ft Q5 \end a 
  \ft Q6 \end používa dokazovač automaticky. 

theory Peano_indrule logic: 'cl'

fun/2 Mul 'Times_na_d'
  Mul(0,y) = 0
  Mul(S(x),y) = Mul(x,y)+y

thm T8
  Mul(x,0) = 0
proof 
 ind N1; x @ 0; x
  proved
  proved..

rem 
  \para Konštanta \ft 1 \end je skratkou za \ft S(0) \end (podobne aj ďalšie 
  číselné konštanty). 

thm Auto1
  1 = S(0)
proof  proved.

thm T9
  Mul(x,1) = x
proof 
 ind N1; x @ 0; x
  proved
  proved..

thm Auto2
  1+x = S(x)
proof  proved.

thm T10
  Mul(x,y+z) = Mul(x,y)+Mul(x,z)
proof 
 ind N1; x @ 0; x
  proved
  proved..

thm T11
  Mul(x,y) = Mul(y,x)
proof 
 ind N1; x @ 0; x
  use T8; y proved.
  use T9; y
   use T10; y; 1; x proved....

thm T12
  Mul(x+y,z) = Mul(x,z)+Mul(y,z)
proof 
 ind N1; z @ 0; z
  use T8; x
   use T8; y
    use T8; x+y proved...
  use T10; x+y; 1; z
   use T9; x+y
    use T10; y; 1; z
     use T9; y
      use T10; x; 1; z
       use T9; x proved........

thm T13
  Mul(Mul(x,y),z) = Mul(x,Mul(y,z))
proof 
 ind N1; x @ 0; x
  proved
  use T12; y; Mul(x,y); z proved...

rem 
  \para Na tento dôkaz budete potrebovať variant pravidla matematickej 
  indukcie: 
  \eq* 
    Split_rule2(Goal Phi2_d(x,y),Goal Phi2_d(0,y),
                Goal Impl(Forall(y,Phi2_d(x,y)),Phi2_d(S(x),y)))
  \end
  \para ktorý použijete príkazom \bf  ind*  \end \ft N1 \end; \ft x \end; 
  \ft y \end. 

thm T14
  z != 0 -> Mul(x,z) = Mul(y,z) <-> x = y
proof 
 case N1; z @ 0; z1
  proved
  ind* N1; x; y @ 0; x
   split* Mul(y,S(z1)) = 0 <-> y = 0.2,0,0
    use T8; S(z1)
     case N1; y @ 0; y1
      proved
      proved..
    proved.
   split* z1+Mul(x,S(z1))+1 = Mul(y,S(z1)) <-> S(x) = y.2,0,0
    case N1; y @ 0; y1
     proved
     inst \a y(Mul(y1,S(z1)) = Mul(y,S(z1)) <-> x = y).0; y1 proved..
    proved....

thm T15
  z != 0 -> Mul(z,x) = Mul(z,y) <-> x = y
proof 
 case N1; z @ 0; z1
  proved
  use T11; z1; x
   use T11; z1; y
    use T14.0; z; x; y
     use T10; x; 1; z1
      use T10; y; 1; z1
       use T9; x
        use T9; y proved.........

end theory Peano_indrule