---

Step * 1 3 of Lemma aa_kleene_fan_contra2


1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. x : @i
 l: List. ((x = ||l||)  ((l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) l))
BY
{ ((InstLemma `mklist_length` [y.if f y y then ff else tt fi ;x]
    THEN Auto
    THEN (Assert x = ||mklist(x;y.if f y y then ff else tt fi )|| BY
                MaAuto))
   THEN (Reduce 0 THEN (InstConcl [mklist(x;y.if f y y then ff else tt fi )] THENA Auto))
   THEN Auto) }

1
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. x : @i
5. ||mklist(x;y.if f y y then ff else tt fi )|| ~ x
6. x = ||mklist(x;y.if f y y then ff else tt fi )||
7. y : @i
8. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
9. f y y = ff@i
 mklist(x;y.if f y y then ff else tt fi )[y] = tt

2
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. x : @i
5. ||mklist(x;y.if f y y then ff else tt fi )|| ~ x
6. x = ||mklist(x;y.if f y y then ff else tt fi )||
7. y : @i
8. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
9. f y y = tt@i
 mklist(x;y.if f y y then ff else tt fi )[y] = ff



1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
2.  \mforall{}a1,a2:\mBbbN{}.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))@i
3.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
4.  x  :  \mBbbN{}@i
\mvdash{}  \mexists{}l:\mBbbB{}  List
      ((x  =  ||l||)
      \mwedge{}  ((\mlambda{}l.\mforall{}y:\mBbbN{}.  ((y  <  ||l||)  {}\mRightarrow{}  ((f  y  y  =  ff  {}\mRightarrow{}  l[y]  =  tt)  \mwedge{}  (f  y  y  =  tt  {}\mRightarrow{}  l[y]  =  ff))))  l))


By

((InstLemma  `mklist\_length`  [\mkleeneopen{}\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  \mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
    THEN  Auto
    THEN  (Assert  x  =  ||mklist(x;\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  )||  BY
                            MaAuto))
  THEN  (Reduce  0  THEN  (InstConcl  [\mkleeneopen{}mklist(x;\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  )\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  Auto)



Home Index