Step
*
1
3
2
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. x : 
@i
7. g : y:
 
 m:
 
 (
nsteps:
m. (
(T y nsteps)) + (
(
nsteps:
m. (
(T y nsteps)))))
 
y,m:
.  (
nsteps:
m. (
(T y nsteps)) 

 
((
y,m. isl(g y m)) y m))
BY
{ (Reduce 0 THEN (UnivCD THENA 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. x : 
@i
7. g : y:
 
 m:
 
 (
nsteps:
m. (
(T y nsteps)) + (
(
nsteps:
m. (
(T y nsteps)))))
8. y : 
@i
9. m : 
@i
 
nsteps:
m. (
(T y nsteps)) 

 
isl(g y m)
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.  x  :  \mBbbN{}@i
7.  g  :  y:\mBbbN{}  {}\mrightarrow{}  m:\mBbbN{}  {}\mrightarrow{}  (\mexists{}nsteps:\mBbbN{}m.  (\muparrow{}(T  y  nsteps))  +  (\mneg{}(\mexists{}nsteps:\mBbbN{}m.  (\muparrow{}(T  y  nsteps)))))
\mvdash{}  \mforall{}y,m:\mBbbN{}.    (\mexists{}nsteps:\mBbbN{}m.  (\muparrow{}(T  y  nsteps))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}((\mlambda{}y,m.  isl(g  y  m))  y  m))
By
(Reduce  0  THEN  (UnivCD  THENA  Auto))
Home
Index