mod Ex11 logic: 'cl'

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

rem 
  \para* \it  Dátum:  \end štvrtok 16. 12. 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 "Cvičenia". 

appldisp/1 F_d
  Std('f',0)

appldisp/3 G_d
  Std('g',0)

appldisp/1 Ms_d
  Prefix(90,2,Id(0,Ent('mu'),0),Arg(0))

appldisp/3 Gnit_d
  Prefix(90,2,Subsup(Id(1,'g',0),75,None,Op(Ent('lowast'),0)),
         Fenced(Op('(',0),
                Infix(Arg(0),30,2,Op(',',0),Infix(Arg(1),30,2,Op(',',0),Arg(2))),
                Op(')',0)))

appldisp/1 Fact_d
  Postfix(Arg(0),60,1,Op('!',0))

appldisp/0 Cdots
  Op(Ent('ctdot'),0)

fun/0 Fill_in 'Cdots'
  Fill_in = 2004

theory Pair_less_thy

axiom Pair_less
  x < x,y & y < x,y

rem 
  \para \bf  C V I Č E N I A  \end 

rem 
  \para \it  \bf  Introduction of some functions into PA by clausal definitions 
  which are reduced to nested recursion  \end  \end 

rem 
  \para V tomto cvičení si na viacerých príkladoch vyskúšate, ako sa 
  rekurzívne klauzálne definície redukujú do \it  schémy vnorenej iterácie 
   \end (schema of nested iteration), ktorú sme dokazovali v cvičení Ex09. 

theory Nested_iter

fun/0 C 

fun/3 G 'G_d'

fun Ms 'Ms_d'

axiom Regularity_major
  G(x,n,a) = S1(v) -> Ms(v) < Ms(x)

axiom Regularity_minor
  \e v G(x,0,a) = S0(v)

fun/3 Gnit 'Gnit_d'
  Gnit(x,n,a) = v <- G(x,n,a) = S0(v)
  Gnit(x,n,a) = y <- 
    G(x,n,a) = S1(v) & n = m+1 & Gnit(v,C,0) = w & Gnit(x,m,a++(w,0)) = y

end theory Nested_iter

rem 
  \para Schéma hovorí, že ak nájdeme konštantu \ft C \end, funkciu 
  \ft G_d(x,n,a) \end a funkciu \ft Ms_d(x) \end, ktoré spĺňajú podmienky 
  \ft Regularity_major \end a \ft Regularity_minor \end, existuje funkcia 
  \ft Gnit_d(x,n,a) \end s uvedenými klauzulami. 
  \para Funkcia \ft Gnit_d(x,n,a) \end simuluje rekurzívny výpočet riadený 
  funkciou \ft G_d(x,n,a) \end. Ak \ft G_d(x,n,a) \end vráti číslo s nulovým 
  posledným bitom, výpočet sa končí a jeho výsledkom je hodnota vrátená 
  funkciou \ft g \end bez posledného bitu. Ak \ft G_d(x,n,a) \end vráti 
  číslo s jednotkový posledným bitom, toto číslo (po odstránení 
  posledného bitu), \ft v \end, je argumentom rekurzívneho volania. Miera 
  argumentu \ft v \end pritom musí byť menšia ako miera \ft x \end (podmienka 
  \ft Regularity_major \end). 
  \para Výsledok \ft w \end rekurzívneho volania je uložený na koniec 
  akumulátora \ft a \end a výpočet pokračuje opätovným volaním riadiacej 
  funkcie \ft g \end s pôvodným argumentom \ft x \end, o jedna zníženým 
  počítadlom rekurzívnych volaní (druhý argument, inicializovaný 
  konštantou \ft C \end) a novým akumulátorom. Ak počítadlo klesne na nulu, 
  funkcia \ft g \end musí ukončiť výpočet vrátením párneho čísla 
  (podmienka \ft Regularity_minor \end). 

rem 
  \para Na to, aby sme funkciu \ft F_d(x) \end danú rekurzívnou klauzálnou 
  definíciou s mierou \ft Ms_d(x) \end mohli zaviesť do Peanovej aritmetiky, 
  musíme urobiť nasledovné: 
  \points 
   \item \para Určiť konštantu \ft C \end (je rovná najväčšiemu počtu 
         rekurzívnych volaní v jednej klauzule v rekurzívnej definícii). 
   \item \para Preložiť rekurzívnu definíciu do zodpovedajúcej 
         nerekurzívnej funkcie \ft g \end. 
   \item \para Dokázať podmienky regularity. 
   \item \para Definovať funkciu \ft F_d(x) \end ako rovnú 
         \ft Gnit_d(x,C,0) \end. 
   \item \para Dokázať klauzuly rekurzívnej definície ako teorémy. 
  \end
  \para Pomocou vnorenej iterácie môžeme definovať aj funkcie s viac ako 
  jedným argumentom -- argumenty spárujeme. 

rem 
  \para \bf  Príklad 1.  \end Zavedieme funkciu \ft Sum(x) \end s klauzálnou 
  definíciou: 
  \def 
    fun Sum 
    Sum(0) = 0
    Sum(x+1) = x+1+Sum(x)
  \end
  \para Mierou tejto definície je identita, teda \ft Ms_d(x) = x \end. Navyše 
  vidíme, že najväčší počet rekurzívnych volaní v jednej klauzule je 
  \ft 1 \end, preto \ft C = 1 \end. 
  \para Definíciu upravíme zavedením výstupnej premennej a priradením 
  hodnoty každého rekurzívneho volania do novej pomocnej premennej v tele 
  klauzuly: 
  \def* 
    Sum(0) = v <- 0 = v
    Sum(x+1) = v <- Sum(x) = u & x+1+u = v
  \end
  \para Funkciu \ft G_d(x,n,a) \end skonštruujeme takto: 
  \points 
   \item \para K výsledku funkcie v každej klauzule pridáme nulový bit. 
   \item \para Každé rekurzívne volanie vo funkcii \ft Sum \end nahradíme 
         \it  párovou diskrimináciou akumulátora \ft a \end  \end. Ak je 
         akumulátor prázdny, vrátime \it  argument rekurzívneho volania 
          \end s pridaným jednotkovým bitom, ale len za podmienky, že 
         počítadlo rekurzií \ft n \end nie je nulové (inak by sme neskôr 
         nemohli dokázať \ft Regularity_minor \end). Ak je akumulátor 
         neprázdny, jeho prvý prvok použijeme ako \it  výsledok 
         rekurzívneho volania  \end. 
  \end
  \para Výsledkom tohto prekladu bude funkcia 
  \def 
    fun/3 G 'G_d'
    G(0,n,a) = v <- S0(0) = v
    G(x+1,n,a) = v <- a = 0 & n > 0 & S1(x) = v
    G(x+1,n,a) = v <- a = u,b & S0(x+1+u) = v
  \end
  \para Teraz môžeme vložiť lokálnu \it  interpretáciu teórie 
  \ft Nested_iter \end  \end (Ins/Del > Insert > Interpretation of a theory). V 
  nej vyplníme definície konštanty \ft C \end, funkcie \ft G(x,n,a) \end a 
  funkcie \ft Ms_d(x) \end a dokážeme podmienky regularity. 
  \para Funkciu \ft Sum \end potom definujeme ako 
  \ft Sum(x) = Gnit_d(x,C,0) \end a dokážeme jej klauzuly. 

loc interpretation of Nested_iter

int fun/0 C 
  C = 1

int fun/3 G 'G_d'
  G(0,n,a) = v <- S0(0) = v
  G(x+1,n,a) = v <- a = 0 & n > 0 & S1(x) = v
  G(x+1,n,a) = v <- a = u,b & S0(x+1+u) = v

int fun Ms 'Ms_d'
  Ms(x) = x

int thm Regularity_major
proof 
 case N; x @ 0; y
  proved
  case P; a @ 0; u,b
   cut n > 0
    proved
    proved.
   proved...

int thm Regularity_minor
proof 
 case N; x @ 0; y
  inst* \e v v = 0; 0 proved.
  case P; a @ 0; u,b
   inst* \e v v = 0; 0 proved.
   inst* \e v u+y+1 = v; u+y+1 proved....

int fun/3 Gnit 'Gnit_d'

fun Sum 
  Sum(x) = Gnit(x,C,0)

thm Sum0
  Sum(0) = 0
proof  proved.

thm Sum1
  Sum(x+1) = x+1+Sum(x)
proof  proved.

end interpretation of Nested_iter

rem 
  \para \bf  Cvičenie 1.  \end Pomocou vnorenej iterácie zadefinujte funkciu 
  \ft Fact(x) \end a dokážte jej klauzuly 
  \def 
    fun Fact 'Fact_d'
    Fact(0) = 1
    Fact(x+1) = (x+1)*Fact(x)
  \end

loc interpretation of Nested_iter

int fun/0 C 
  C = 1

int fun/3 G 'G_d'
  G(0,n,a) = v <- S0(1) = v
  G(x+1,n,a) = v <- a = 0 & n > 0 & S1(x) = v
  G(x+1,n,a) = v <- a = u,b & S0((x+1)*u) = v

int fun Ms 'Ms_d'
  Ms(x) = x

int thm Regularity_major
proof 
 case N; x @ 0; x1
  proved
  case P; a @ 0; u,b
   case N; n @ 0; n1
    proved
    proved.
   proved...

int thm Regularity_minor
proof 
 case N; x @ 0; x1
  inst* \e v v = 1; 1 proved.
  case P; a @ 0; v,w
   inst* \e v v = 0; 0 proved.
   inst* \e v1 v+v*x1 = v1; v+v*x1 proved....

int fun/3 Gnit 'Gnit_d'

fun Fact 'Fact_d'
  Fact(x) = Gnit(x,C,0)

thm Fact0
  Fact(0) = 1
proof  proved.

thm Fact1
  Fact(n+1) = (n+1)*Fact(n)
proof  proved.

end interpretation of Nested_iter

rem 
  \para \bf  Príklad 2.  \end Do Peanovej aritmetiky chceme zaviesť funkciu 
  \def 
    fun Fib 
    Fib(0) = 1
    Fib(1) = 1
    Fib(x+2) = Fib(x)+Fib(x+1)
  \end
  \para Najväčší počet rekurzívnych volaní v jednej klauzule je 
  \ft 2 \end, teda \ft C = 2 \end a mierou tejto definície je 
  \ft Ms_d(x) = x \end. Vykonáme obligátne úpravy -- zavedenie výstupnej 
  premennej a zavedenie premenných pre hodnoty rekurzívnych volaní: 
  \def* 
    Fib(0) = v <- 1 = v
    Fib(1) = v <- 1 = v
    Fib(x+2) = v <- Fib(x) = u & Fib(x+1) = z & u+z = v
  \end
  \para Všimnite si, že keď teraz chceme skonštruovať funkciu 
  \ft G_d(x,n,a) \end, pri odstraňovaní \it  druhého rekurzívneho volania 
   \end musíme aplikovať párovú diskrimináciu na \it  chvost akumulátora 
   \end (nazvali sme ho \ft b \end). 
  \def* 
    G_d(0,n,a) = v <- S0(1) = v
    G_d(1,n,a) = v <- S0(1) = v
    G_d(x+2,n,a) = v <- a = 0 & n > 0 & S1(x) = v
    G_d(x+2,n,a) = v <- a = u,b & b = 0 & n > 0 & S1(x+1) = v
    G_d(x+2,n,a) = v <- a = u,b & b = z,c & S0(u+z) = v
  \end

rem 
  \para \bf  Cvičenie 2.  \end Dokončite príklad 2. 

loc interpretation of Nested_iter

int fun/0 C 
  C = 2

int fun/3 G 'G_d'
  G(0,n,a) = v <- S0(1) = v
  G(1,n,a) = v <- S0(1) = v
  G(x+2,n,a) = v <- a = 0 & n > 0 & S1(x) = v
  G(x+2,n,a) = v <- a = b,e & e = 0 & n > 0 & S1(x+1) = v
  G(x+2,n,a) = v <- a = b,e & e = c,d & S0(b+c) = v

int fun Ms 'Ms_d'
  Ms(x) = x

int thm Regularity_major
proof 
 case N; x @ 0; x1
  proved
  case N; x1 @ 0; x2
   proved
   case P; a @ 0; v1,w
    case N; n @ 0; n1
     proved
     proved.
    case P; w @ 0; v2,w1
     case N; n @ 0; n1
      proved
      proved.
     proved.....

rem 
  \para Pozorny citatel doplni inst*-y. 

int thm Regularity_minor
proof 
 case N; x @ 0; x1
  conj
  case N; x1 @ 0; x2
   conj
   case P; a @ 0; v,w
    conj
    case P; w @ 0; v1,w1
     conj
     conj.....

int fun/3 Gnit 'Gnit_d'

fun Fib 
  Fib(x) = Gnit(x,C,0)

thm Thm1
  Fib(0) = 1
proof  proved.

thm Thm2
  Fib(1) = 1
proof  proved.

thm Thm3
  Fib(x+2) = Fib(x+1)+Fib(x)
proof  proved.

end interpretation of Nested_iter

rem 
  \para \bf  Cvičenie 3.  \end Pomocou vnorenej iterácie zadefinujte funkciu 
  \ft L(x) \end a dokážte jej klauzuly 
  \def 
    fun L 
    L(0) = 0
    L(h,t) = L(t)+1
  \end
  \para Pri dôkaze regularity budete potrebovať vlastnosť 
  \ft x < x,y & y < x,y \end, ktorá nie je zabudovaná do dokazovača CL, ale 
  dodali sme ju ako axiómu \ft Pair_less \end. 

loc interpretation of Nested_iter

int fun/0 C 
  C = 1

int fun/3 G 'G_d'
  G(0,n,a) = v <- S0(0) = v
  G((p,q),n,a) = v <- a = 0 & n > 0 & S1(q) = v
  G((p,q),n,a) = v <- a = b,c & S0(1+b) = v

int fun Ms 'Ms_d'
  Ms(x) = x

int thm Regularity_major
proof 
 case P; x @ 0; v1,w
  proved
  case P; a @ 0; v2,w1
   case N; n @ 0; n1
    proved
    use Pair_less.4,1,0; v1; v proved..
   proved...

int thm Regularity_minor
proof 
 case P; x @ 0; v,w
  inst* \e v v = 0; 0 proved.
  case P; a @ 0; v1,w1
   inst* \e v1 v1 = 0; 0 proved.
   inst* \e v2 v1+1 = v2; v1+1 proved....

int fun/3 Gnit 'Gnit_d'

fun L 
  L(x) = Gnit(x,C,0)

thm Thm1
  L(0) = 0
proof  proved.

thm Thm2
  L(a,b) = 1+L(b)
proof  proved.

end interpretation of Nested_iter

rem 
  \para \bf  Cvičenie 4.  \end Pomocou vnorenej iterácie zadefinujte funkciu 
  \it  Pre(t,b)  \end, ktorá vytvorí zoznam prvkov stromu \ft t \end v poradí 
  \it  pre-order  \end pomocou akumulátora \ft b \end a dokážte jej klauzuly. 
  \para Strom je konštruovaný z prázdnych stromov \ft 0 \end a uzlov 
  \ft k,l,r \end, kde \ft k \end je hodnota uložená v uzle (kľúč, návestie 
  , key, label) a \ft l \end resp. \ft r \end sú ľavý resp. pravý podstrom. 
  \def 
    fun/2 Pre 
    Pre(t,b) = z <- t = 0 & b = z
    Pre(t,b) = z <- t = k,l,r & Pre(r,b) = pr & Pre(l,pr) = plr & k,plr = z
  \end
  \para Návod nájdete v CL súbore lec11.cl na stránke. 

loc interpretation of Nested_iter

int fun/0 C 
  C = 2

int fun/3 G 'G_d'
  G((0,b),n,a) = v <- S0(b) = v
  G(((k,l,r),b),n,a) = v <- a = 0 & n > 0 & S1(r,b) = v
  G(((k,l,r),b),n,a) = v <- a = a1,w1 & w1 = 0 & n > 0 & S1(l,a1) = v
  G(((k,l,r),b),n,a) = v <- a = a1,w1 & w1 = a2,w2 & S0(k,a2) = v

int fun Ms 'Ms_d'
  Ms(t,b) = t

int thm Regularity_major
proof 
 case P; x @ 0; t,b
  proved
  case P; t @ 0; k,p
   proved
   case P; p @ 0; l,r
    proved
    case P; a @ 0; a1,w1
     case N; n @ 0; n1
      proved
      use Pair_less.4,1,0; l; r
       use Pair_less.4,1,0; k; l,r proved...
     case P; w1 @ 0; a2,w2
      case N; n @ 0; n1
       proved
       use Pair_less.4,0,0; l; r
        use Pair_less.4,1,0; k; l,r proved...
      proved......

int thm Regularity_minor
proof 
 case P; x @ 0; t,b
  inst* \e v v = 0; 0 proved.
  case P; t @ 0; k,p
   inst* \e v b = v; b proved.
   case P; p @ 0; l,r
    inst* \e v v = 0; 0 proved.
    case P; a @ 0; a1,w1
     inst* \e v v = 0; 0 proved.
     case P; w1 @ 0; a2,w2
      inst* \e v v = 0; 0 proved.
      inst* \e v k,a2 = v; k,a2 proved.......

int fun/3 Gnit 'Gnit_d'

fun/2 Pre 
  Pre(t,b) = Gnit((t,b),C,0)

thm Pre0
  Pre(0,b) = b
proof  proved.

thm Pre1
  Pre((k,l,r),b) = k,Pre(l,Pre(r,b))
proof  proved.

end interpretation of Nested_iter

rem 
  \para \bf  Cvičenie 5.  \end Zadefinujete nasledujúce funkcie pomocou 
  vnorenej iterácie a dokážte ich klauzuly (vrátane defaultových!). 

rem 
  \para Postorder 
  \def 
    fun/2 Post 
    Post(t,b) = z <- t = 0 & b = z
    Post(t,b) = z <- t = k,l,r & Post(r,k,b) = pr & Post(l,pr) = z
  \end

loc interpretation of Nested_iter

int fun/0 C 
  C = 2

int fun/3 G 'G_d'
  G((0,b),n,a) = v <- S0(b) = v
  G(((k,l,r),b),n,a) = v <- a = 0 & n > 0 & S1(r,k,b) = v
  G(((k,l,r),b),n,a) = v <- a = a1,w1 & w1 = 0 & n > 0 & S1(l,a1) = v
  G(((k,l,r),b),n,a) = v <- a = a1,w1 & w1 = a2,w2 & S0(a2) = v

int fun Ms 'Ms_d'
  Ms(t,b) = t

int thm Regularity_major
proof 
 case P; x @ 0; t,b
  proved
  case P; t @ 0; k,p
   proved
   case P; p @ 0; l,r
    proved
    case P; a @ 0; a1,w1
     case N; n @ 0; n1
      proved
      use Pair_less.4,1,0; k; l,r
       use Pair_less.4,1,0; l; r proved...
     case P; w1 @ 0; v1,w
      case N; n @ 0; n1
       proved
       use Pair_less.4,0,0; l; r
        use Pair_less.4,1,0; k; l,r proved...
      proved......

int thm Regularity_minor
proof 
 case P; x @ 0; t,b
  inst* \e v v = 0; 0 proved.
  case P; t @ 0; k,p
   inst* \e v b = v; b proved.
   case P; p @ 0; l,r
    inst* \e v v = 0; 0 proved.
    case P; a @ 0; a1,w1
     inst* \e v v = 0; 0 proved.
     case P; w1 @ 0; a2,w2
      inst* \e v v = 0; 0 proved.
      inst* \e v a2 = v; a2 proved.......

int fun/3 Gnit 'Gnit_d'

fun/2 Post 
  Post(t,b) = Gnit((t,b),C,0)

thm Post0
  Post(0,b) = b
proof  proved.

thm Post1
  Post((k,l,r),b) = Post(l,Post(r,k,b))
proof  proved.

end interpretation of Nested_iter

rem 
  \def 
    fun Fib3 
    Fib3(n) = z <- n = 0 & 0 = z
    Fib3(n) = z <- n = 1 & 1 = z
    Fib3(n) = z <- n = 2 & 2 = z
    Fib3(n) = z <- 
      n = k+3 & Fib3(k) = a & Fib3(k+1) = b & Fib3(k+2) = c & a+b+c = z
  \end

loc interpretation of Nested_iter

int fun/0 C 
  C = 3

int fun/3 G 'G_d'
  G(0,n,a) = v <- S0(0) = v
  G(1,n,a) = v <- S0(1) = v
  G(2,n,a) = v <- S0(2) = v
  G(x+3,n,a) = v <- a = 0 & n > 0 & S1(x) = v
  G(x+3,n,a) = v <- a = a1,w1 & w1 = 0 & n > 0 & S1(x+1) = v
  G(x+3,n,a) = v <- a = a1,w1 & w1 = a2,w2 & w2 = 0 & n > 0 & S1(x+2) = v
  G(x+3,n,a) = v <- a = a1,w1 & w1 = a2,w2 & w2 = a3,w3 & S0(a1+a2+a3) = v

int fun Ms 'Ms_d'
  Ms(x) = x

int thm Regularity_major
proof 
 case N; x @ 0; x1
  proved
  case N; x1 @ 0; x2
   proved
   case N; x2 @ 0; x3
    proved
    case P; a @ 0; a1,w1
     case N; n @ 0; n1
      proved
      proved.
     case P; w1 @ 0; a2,w2
      case N; n @ 0; n1
       proved
       proved.
      case P; w2 @ 0; a3,w3
       case N; n @ 0; n1
        proved
        proved.
       proved.......

int thm Regularity_minor
proof 
 case N; x @ 0; x1
  conj
  case N; x1 @ 0; x2
   conj
   case N; x2 @ 0; x3
    conj
    case P; a @ 0; a1,w1
     conj
     case P; w1 @ 0; a2,w2
      conj
      case P; w2 @ 0; a3,w3
       conj
       inst* \e v a1+a2+a3 = v; a1+a2+a3 proved........

int fun/3 Gnit 'Gnit_d'

fun Fib3 
  Fib3(x) = Gnit(x,C,0)

thm Fib0
  Fib3(0) = 0
proof  proved.

thm Fib1
  Fib3(1) = 1
proof  proved.

thm Fib2
  Fib3(2) = 2
proof  proved.

thm Fib33
  Fib3(x+3) = Fib3(x+2)+Fib3(x+1)+Fib3(x)
proof  proved.

end interpretation of Nested_iter

rem 
  \para Maximum zoznamu 
  \def 
    fun Maxl 
    Maxl(n) = z <- n = 0 & 0 = z
    Maxl(n) = z <- n = a,b & Maxl(b) = x & a <= x & x = z
    Maxl(n) = z <- n = a,b & Maxl(b) = x & a > x & a = z
  \end

loc interpretation of Nested_iter

int fun/0 C 
  C = 1

int fun/3 G 'G_d'
  G(0,n,a) = v <- S0(0) = v
  G((p,q),n,a) = v <- a = 0 & n > 0 & S1(q) = v
  G((p,q),n,a) = v <- a = a1,w1 & p <= a1 & S0(a1) = v
  G((p,q),n,a) = v <- a = a1,w1 & p > a1 & S0(p) = v

int fun Ms 'Ms_d'
  Ms(x) = x

int thm Regularity_major
proof 
 case P; x @ 0; p,q
  proved
  case P; a @ 0; a1,w1
   case N; n @ 0; n1
    proved
    use Pair_less.4,1,0; p; v proved..
   cut p <= a1
    proved
    proved....

int thm Regularity_minor
proof 
 case P; x @ 0; p,q
  inst* \e v v = 0; 0 proved.
  case P; a @ 0; a1,w1
   inst* \e v v = 0; 0 proved.
   cut p <= a1
    inst* \e v a1 = v; a1 proved.
    inst* \e v p = v; p proved.....

int fun/3 Gnit 'Gnit_d'

fun Maxl 
  Maxl(x) = Gnit(x,C,0)

thm Maxl0
  Maxl(0) = 0
proof  proved.

thm Maxl1
  x > Maxl(y) -> Maxl(x,y) = x
proof  proved.

thm Maxl2
  x <= Maxl(y) -> Maxl(x,y) = Maxl(y)
proof  proved.

end interpretation of Nested_iter

rem 
  \para Umocňovanie 
  \def 
    fun/2 Exp 
    Exp(x,y) = z <- y = 0 & 1 = z
    Exp(x,y) = z <- y = k+1 & Exp(x,k) = v & x*v = z
  \end

loc interpretation of Nested_iter

int fun/0 C 
  C = 1

int fun/3 G 'G_d'
  G((x,0),n,a) = v <- S0(1) = v
  G((x,y+1),n,a) = v <- a = 0 & n > 0 & S1(x,y) = v
  G((x,y+1),n,a) = v <- a = a1,w1 & S0(x*a1) = v

int fun Ms 'Ms_d'
  Ms(x,y) = y

int thm Regularity_major
proof 
 case P; x @ 0; x1,y
  proved
  case N; y @ 0; y1
   proved
   case P; a @ 0; v1,w
    case N; n @ 0; n1
     proved
     proved.
    proved....

int thm Regularity_minor
proof 
 case P; x @ 0; x1,y
  inst* \e v v = 0; 0 proved.
  case N; y @ 0; y1
   inst* \e v v = 1; 1 proved.
   case P; a @ 0; v,w
    inst* \e v v = 0; 0 proved.
    inst* \e v1 v*x1 = v1; v*x1 proved.....

int fun/3 Gnit 'Gnit_d'

fun/2 Exp 
  Exp(x,y) = Gnit((x,y),C,0)

thm Exp0
  Exp(x,0) = 1
proof  proved.

thm Exp1
  Exp(x,y+1) = x*Exp(x,y)
proof  proved.

end interpretation of Nested_iter

end theory Pair_less_thy