---

Step * 1 3 2 of Lemma aa_kleene_fan_contra


1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. x : @i
5. y : @i
6. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
7. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
8. f y y = ff@i
 mklist(x;y.if f y y then ff else tt fi )[y] = tt
BY
{ (InstLemma `mklist_select` [;x;y.if f y y then ff else tt fi ;y] THENA 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. y : @i
6. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
7. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
8. f y y = ff@i
 y < x

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. y : @i
6. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
7. y < ||mklist(x;y.if f y y then ff else tt fi )||@i
8. f y y = ff@i
9. mklist(x;y.if f y y then ff else tt fi )[y] = (y.if f y y then ff else tt fi ) y
 mklist(x;y.if f y y then ff else tt fi )[y] = tt



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
5.  y  :  \mBbbN{}@i
6.  y  <  ||mklist(x;\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  )||@i
7.  y  <  ||mklist(x;\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  )||@i
8.  f  y  y  =  ff@i
\mvdash{}  mklist(x;\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  )[y]  =  tt


By

(InstLemma  `mklist\_select`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}y.if  f  y  y  then  ff  else  tt  fi  \mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)



Home Index