---

Step * 1 1 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. l1 :  List@i
5. l2 :  List@i
6. (l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) (l1 @ l2)@i
 (l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) l1
BY
{ ((Reduce 0 THEN Reduce (-1))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstHyp [y] (-3) THENA Auto)
   THEN skip{easy}) }

1
.....antecedent..... 
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. l1 :  List@i
5. l2 :  List@i
6. y:. ((y < ||l1 @ l2||)  ((f y y = ff  l1 @ l2[y] = tt)  (f y y = tt  l1 @ l2[y] = ff)))@i
7. y : @i
8. y < ||l1||@i
 y < ||l1 @ l2||

2
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. l1 :  List@i
5. l2 :  List@i
6. y:. ((y < ||l1 @ l2||)  ((f y y = ff  l1 @ l2[y] = tt)  (f y y = tt  l1 @ l2[y] = ff)))@i
7. y : @i
8. y < ||l1||@i
9. (f y y = ff  l1 @ l2[y] = tt)  (f y y = tt  l1 @ l2[y] = ff)
 (f y y = ff  l1[y] = tt)  (f y y = tt  l1[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.  l1  :  \mBbbB{}  List@i
5.  l2  :  \mBbbB{}  List@i
6.  (\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))))  (l1  @  l2)@i
\mvdash{}  (\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))))  l1


By

((Reduce  0  THEN  Reduce  (-1))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  skip\{easy\})



Home Index