Step * 1 2 2 1 1 1 of Lemma aa_kleene_fan_contra4


1. f :     bar()@i
2. b:  bar(). a:. ((f a) = b)@i
3. T :     @i
4. i,nsteps:.  (((T i nsteps))  (f i i))@i
5. i:. ((f i i)  (nsteps:. ((T i nsteps))))@i
6. A :   @i
7. a : 
8. (f a) = A
9. (f a) = A
10. (A a)
11. (f a a)
12. nsteps : 
13. (T a nsteps)
 (y:
      ((y < ||mklist(a + nsteps + 1;A)||)
       ((((nsteps@0:. ((nsteps@0 < ||mklist(a + nsteps + 1;A)||)  ((T y nsteps@0))))  f y y = ff)
          mklist(a + nsteps + 1;A)[y] = tt)
          (((nsteps@0:. ((nsteps@0 < ||mklist(a + nsteps + 1;A)||)  ((T y nsteps@0))))  f y y = tt)
            mklist(a + nsteps + 1;A)[y] = ff))))
BY
{ ((Assert 0  (a + nsteps + 1) BY
          MaAuto)
   THEN (D 0
         THEN Auto
         THEN InstLemma `mklist_length` [A;a + nsteps + 1]
         THEN Auto
         THEN (Assert ||mklist(a + nsteps + 1;A)|| = (a + nsteps + 1) BY
                     MaAuto)
         THEN Try (Complete ((RepeatFor 2 (D (-3)) THEN Termination THEN Auto))))
   ) }

1
1. f :     bar()@i
2. b:  bar(). a:. ((f a) = b)@i
3. T :     @i
4. i,nsteps:.  (((T i nsteps))  (f i i))@i
5. i:. ((f i i)  (nsteps:. ((T i nsteps))))@i
6. A :   @i
7. a : 
8. (f a) = A
9. (f a) = A
10. (A a)
11. (f a a)
12. nsteps : 
13. (T a nsteps)
14. 0  (a + nsteps + 1)
15. y:
      ((y < ||mklist(a + nsteps + 1;A)||)
       ((((nsteps@0:. ((nsteps@0 < ||mklist(a + nsteps + 1;A)||)  ((T y nsteps@0))))  f y y = ff)
          mklist(a + nsteps + 1;A)[y] = tt)
          (((nsteps@0:. ((nsteps@0 < ||mklist(a + nsteps + 1;A)||)  ((T y nsteps@0))))  f y y = tt)
            mklist(a + nsteps + 1;A)[y] = ff)))@i
16. ||mklist(a + nsteps + 1;A)|| ~ a + nsteps + 1
17. ||mklist(a + nsteps + 1;A)|| = (a + nsteps + 1)
 False



1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})@i
2.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
3.  T  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
4.  \mforall{}i,nsteps:\mBbbN{}.    ((\muparrow{}(T  i  nsteps))  {}\mRightarrow{}  (f  i  i)\mdownarrow{})@i
5.  \mforall{}i:\mBbbN{}.  ((f  i  i)\mdownarrow{}  {}\mRightarrow{}  (\mexists{}nsteps:\mBbbN{}.  (\muparrow{}(T  i  nsteps))))@i
6.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
7.  a  :  \mBbbN{}
8.  (f  a)  =  A
9.  (f  a)  =  A
10.  (A  a)\mdownarrow{}
11.  (f  a  a)\mdownarrow{}
12.  nsteps  :  \mBbbN{}
13.  \muparrow{}(T  a  nsteps)
\mvdash{}  \mneg{}(\mforall{}y:\mBbbN{}
            ((y  <  ||mklist(a  +  nsteps  +  1;A)||)
            {}\mRightarrow{}  ((((\mexists{}nsteps@0:\mBbbN{}.  ((nsteps@0  <  ||mklist(a  +  nsteps  +  1;A)||)  \mwedge{}  (\muparrow{}(T  y  nsteps@0))))
                  \mwedge{}  f  y  y  =  ff)
                  {}\mRightarrow{}  mklist(a  +  nsteps  +  1;A)[y]  =  tt)
                  \mwedge{}  (((\mexists{}nsteps@0:\mBbbN{}.  ((nsteps@0  <  ||mklist(a  +  nsteps  +  1;A)||)  \mwedge{}  (\muparrow{}(T  y  nsteps@0))))
                      \mwedge{}  f  y  y  =  tt)
                      {}\mRightarrow{}  mklist(a  +  nsteps  +  1;A)[y]  =  ff))))


By

((Assert  0  \mleq{}  (a  +  nsteps  +  1)  BY
                MaAuto)
  THEN  (D  0
              THEN  Auto
              THEN  InstLemma  `mklist\_length`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a  +  nsteps  +  1\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  (Assert  ||mklist(a  +  nsteps  +  1;A)||  =  (a  +  nsteps  +  1)  BY
                                      MaAuto)
              THEN  Try  (Complete  ((RepeatFor  2  (D  (-3))  THEN  Termination  THEN  Auto\mcdot{})))\mcdot{})\mcdot{}
  )



Home Index