Quelle  while1.thy

{* Isabelle output from while1.cob*}
(lambda $16.1+i)$16=1+i
(lambda $17.t[t .. 1]=t[t:1])$17=t[t .. 1]=t[t:1]
(lambda $18.i+1)$18=i+1
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda ip1.$19)(t[t:1]-t[t:1])>=0=(t[t:1]-t[t:1])>=0
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t .. 1]=t[t:1]=t[t .. 1]=t[t:1]
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda ip1.$19)(t[t:1]-t[t:1])<0=(t[t:1]-t[t:1])<0
(lambda i.i+$25)i=i+$25
(lambda i.i+$25)i+1=(i+$25)+1
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)>=0=($21-100)>=0
(lambda i.$21)t[t:1]=t[t:1]
(lambda i.$21)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda i.$21)(t[t:1]-t[t:1])>=0=(t[t:1]-t[t:1])>=0
(lambda i.$21)((i-100)>=0)|((t[t:1]-t[t:1])>=0)=(($21-100)>=0)|((t[t:1]-t[t:1])>=0)
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda ip1.$19)(t[t:1]-t[t:1])>=0=(t[t:1]-t[t:1])>=0
(lambda ip1.$19)(($21-100)>=0)|((t[t:1]-t[t:1])>=0)=(($21-100)>=0)|((t[t:1]-t[t:1])>=0)
(lambda $21.i+$25)$21=i+$25
(lambda $21.i+$25)$21-100=(i+$25)-100
(lambda $21.i+$25)($21-100)>=0=((i+$25)-100)>=0
(lambda $21.i+$25)(($21-100)>=0)|((t[t:1]-t[t:1])>=0)=(((i+$25)-100)>=0)|((t[t:1]-t[t:1])>=0)
1:ALL {i::nat,t::nat,ip1::nat}.EX $25::nat.(((i+$25)-100)>=0)|((t[t:1]-t[t:1])>=0)?
   =>   $25=(-1*i)+100 (unn.)
1:ALL {i::nat,t::nat,ip1::nat}.EX $25::nat.(((i+$25)-100)>=0)|((t[t:1]-t[t:1])>=0)?
   =>   $25=(-1*i)+100 (unn.)
(lambda $25.(-1*i)+100)$25=(-1*i)+100
(lambda $25.(-1*i)+100)i+$25=i+((-1*i)+100)
(lambda $25.(-1*i)+100)$25=(-1*i)+100
(lambda $25.(-1*i)+100)$25+1=((-1*i)+100)+1
(lambda $25.(-1*i)+100)i+($25+1)=i+(((-1*i)+100)+1)
(lambda i.i+$26)i=i+$26
(lambda i.i+$26)i+$25=(i+$26)+$25
(lambda i.i+$26)(i+$25)+1=((i+$26)+$25)+1
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)>=0=($21-100)>=0
(lambda i.$21)t[t:1]=t[t:1]
(lambda i.$21)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda i.$21)(t[t:1]-t[t:1])<0=(t[t:1]-t[t:1])<0
(lambda i.$21)((i-100)>=0)|((t[t:1]-t[t:1])<0)=(($21-100)>=0)|((t[t:1]-t[t:1])<0)
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda ip1.$19)(t[t:1]-t[t:1])<0=(t[t:1]-t[t:1])<0
(lambda ip1.$19)(($21-100)>=0)|((t[t:1]-t[t:1])<0)=(($21-100)>=0)|((t[t:1]-t[t:1])<0)
(lambda t.$20)t=$20
(lambda t.$20)t[t:1]=t[$20:1]
(lambda t.$20)t=$20
(lambda t.$20)t[t:1]=t[$20:1]
(lambda t.$20)t[t:1]-t[t:1]=t[$20:1]-t[$20:1]
(lambda t.$20)(t[t:1]-t[t:1])<0=(t[$20:1]-t[$20:1])<0
(lambda t.$20)(($21-100)>=0)|((t[t:1]-t[t:1])<0)=(($21-100)>=0)|((t[$20:1]-t[$20:1])<0)
(lambda $21.i+$26)$21=i+$26
(lambda $21.i+$26)$21-100=(i+$26)-100
(lambda $21.i+$26)($21-100)>=0=((i+$26)-100)>=0
(lambda $21.i+$26)(($21-100)>=0)|((t[$20:1]-t[$20:1])<0)=(((i+$26)-100)>=0)|((t[$20:1]-t[$20:1])<0)
(lambda $20.t[t .. 1]=t[t:1])$20=t[t .. 1]=t[t:1]
(lambda $20.t[t .. 1]=t[t:1])t[$20:1]=t[t[t .. 1]=t[t:1]:1]
(lambda $20.t[t .. 1]=t[t:1])$20=t[t .. 1]=t[t:1]
(lambda $20.t[t .. 1]=t[t:1])t[$20:1]=t[t[t .. 1]=t[t:1]:1]
(lambda $20.t[t .. 1]=t[t:1])t[$20:1]-t[$20:1]=t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1]
(lambda $20.t[t .. 1]=t[t:1])(t[$20:1]-t[$20:1])<0=(t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1])<0
(lambda $20.t[t .. 1]=t[t:1])(((i+$26)-100)>=0)|((t[$20:1]-t[$20:1])<0)=(((i+$26)-100)>=0)|((t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1])<0)
1:ALL {i::nat,t::nat,ip1::nat}.EX $26::nat.(((i+$26)-100)>=0)|((t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1])<0)?
   =>   $26=(-1*i)+100 (unn.)
(lambda $26.(-1*i)+100)$26=(-1*i)+100
(lambda $26.(-1*i)+100)i+$26=i+((-1*i)+100)
(lambda $26.(-1*i)+100)$26=(-1*i)+100
(lambda $26.(-1*i)+100)$26+1=((-1*i)+100)+1
(lambda $26.(-1*i)+100)$25+($26+1)=$25+(((-1*i)+100)+1)
(lambda $26.(-1*i)+100)i+($25+($26+1))=i+($25+(((-1*i)+100)+1))
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)<0=($21-100)<0
(lambda i.$21)t[t:1]=t[t:1]
(lambda i.$21)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda i.$21)(t[t:1]-t[t:1])>=0=(t[t:1]-t[t:1])>=0
(lambda i.$21)((i-100)<0)&&((t[t:1]-t[t:1])>=0)=(($21-100)<0)&&((t[t:1]-t[t:1])>=0)
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda ip1.$19)(t[t:1]-t[t:1])>=0=(t[t:1]-t[t:1])>=0
(lambda ip1.$19)(($21-100)<0)&&((t[t:1]-t[t:1])>=0)=(($21-100)<0)&&((t[t:1]-t[t:1])>=0)
(lambda $21.100)$21=100
(lambda $21.100)$21-100=100-100
(lambda $21.100)($21-100)<0=(100-100)<0
(lambda $21.100)(($21-100)<0)&&((t[t:1]-t[t:1])>=0)=((100-100)<0)&&((t[t:1]-t[t:1])>=0)
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)<0=($21-100)<0
(lambda i.$21)t[t:1]=t[t:1]
(lambda i.$21)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda i.$21)(t[t:1]-t[t:1])<0=(t[t:1]-t[t:1])<0
(lambda i.$21)((i-100)<0)&&((t[t:1]-t[t:1])<0)=(($21-100)<0)&&((t[t:1]-t[t:1])<0)
(lambda ip1.$19)t[t:1]=t[t:1]
(lambda ip1.$19)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda ip1.$19)(t[t:1]-t[t:1])<0=(t[t:1]-t[t:1])<0
(lambda ip1.$19)(($21-100)<0)&&((t[t:1]-t[t:1])<0)=(($21-100)<0)&&((t[t:1]-t[t:1])<0)
(lambda t.$20)t=$20
(lambda t.$20)t[t:1]=t[$20:1]
(lambda t.$20)t=$20
(lambda t.$20)t[t:1]=t[$20:1]
(lambda t.$20)t[t:1]-t[t:1]=t[$20:1]-t[$20:1]
(lambda t.$20)(t[t:1]-t[t:1])<0=(t[$20:1]-t[$20:1])<0
(lambda t.$20)(($21-100)<0)&&((t[t:1]-t[t:1])<0)=(($21-100)<0)&&((t[$20:1]-t[$20:1])<0)
(lambda $21.100)$21=100
(lambda $21.100)$21-100=100-100
(lambda $21.100)($21-100)<0=(100-100)<0
(lambda $21.100)(($21-100)<0)&&((t[$20:1]-t[$20:1])<0)=((100-100)<0)&&((t[$20:1]-t[$20:1])<0)
(lambda $20.t[t .. 1]=t[t:1])$20=t[t .. 1]=t[t:1]
(lambda $20.t[t .. 1]=t[t:1])t[$20:1]=t[t[t .. 1]=t[t:1]:1]
(lambda $20.t[t .. 1]=t[t:1])$20=t[t .. 1]=t[t:1]
(lambda $20.t[t .. 1]=t[t:1])t[$20:1]=t[t[t .. 1]=t[t:1]:1]
(lambda $20.t[t .. 1]=t[t:1])t[$20:1]-t[$20:1]=t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1]
(lambda $20.t[t .. 1]=t[t:1])(t[$20:1]-t[$20:1])<0=(t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1])<0
(lambda $20.t[t .. 1]=t[t:1])((100-100)<0)&&((t[$20:1]-t[$20:1])<0)=((100-100)<0)&&((t[t[t .. 1]=t[t:1]:1]-t[t[t .. 1]=t[t:1]:1])<0)
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)>=0=($21-100)>=0
(lambda $21.100)$21=100
(lambda $21.100)$21-100=100-100
(lambda $21.100)($21-100)>=0=(100-100)>=0
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)>=0=($21-100)>=0
(lambda $21.100)$21=100
(lambda $21.100)$21-100=100-100
(lambda $21.100)($21-100)>=0=(100-100)>=0
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)>=0=($21-100)>=0
(lambda $21.1)$21=1
(lambda $21.1)$21-100=1-100
(lambda $21.1)($21-100)>=0=(1-100)>=0
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)<0=($21-100)<0
(lambda i.$21)t[t:1]=t[t:1]
(lambda i.$21)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda i.$21)(t[t:1]-t[t:1])<0=(t[t:1]-t[t:1])<0
(lambda i.$21)((i-100)<0)&&((t[t:1]-t[t:1])<0)=(($21-100)<0)&&((t[t:1]-t[t:1])<0)
(lambda $21.1)$21=1
(lambda $21.1)$21-100=1-100
(lambda $21.1)($21-100)<0=(1-100)<0
(lambda $21.1)(($21-100)<0)&&((t[t:1]-t[t:1])<0)=((1-100)<0)&&((t[t:1]-t[t:1])<0)
(lambda i.$21)i=$21
(lambda i.$21)i-100=$21-100
(lambda i.$21)(i-100)<0=($21-100)<0
(lambda i.$21)t[t:1]=t[t:1]
(lambda i.$21)t[t:1]-t[t:1]=t[t:1]-t[t:1]
(lambda i.$21)(t[t:1]-t[t:1])>=0=(t[t:1]-t[t:1])>=0
(lambda i.$21)((i-100)<0)&&((t[t:1]-t[t:1])>=0)=(($21-100)<0)&&((t[t:1]-t[t:1])>=0)
(lambda $21.1)$21=1
(lambda $21.1)$21-100=1-100
(lambda $21.1)($21-100)<0=(1-100)<0
(lambda $21.1)(($21-100)<0)&&((t[t:1]-t[t:1])>=0)=((1-100)<0)&&((t[t:1]-t[t:1])>=0)
(lambda konstant.n)konstant=n