let A be preIfWhileAlgebra; for S being non empty set
for T being Subset of S
for f being ExecutionFunction of A,S,T
for I being Element of A
for s being Element of S holds
( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
let S be non empty set ; for T being Subset of S
for f being ExecutionFunction of A,S,T
for I being Element of A
for s being Element of S holds
( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
let T be Subset of S; for f being ExecutionFunction of A,S,T
for I being Element of A
for s being Element of S holds
( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
let f be ExecutionFunction of A,S,T; for I being Element of A
for s being Element of S holds
( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
let I be Element of A; for s being Element of S holds
( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
let s be Element of S; ( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
set g = (curry' f) . I;
hereby ( ((curry' f) . I) orbit s c= T implies not f iteration_terminates_for I,s )
assume A1:
not
f iteration_terminates_for I,
s
;
((curry' f) . I) orbit s c= Tthus
((curry' f) . I) orbit s c= T
verumproof
let x be
object ;
TARSKI:def 3 ( x nin ((curry' f) . I) orbit s or not x nin T )
assume
x in ((curry' f) . I) orbit s
;
not x nin T
then A2:
ex
n being
Element of
NAT st
(
x = (iter (((curry' f) . I),n)) . s &
s in dom (iter (((curry' f) . I),n)) )
;
defpred S1[
Nat]
means (iter (((curry' f) . I),$1)) . s nin T;
assume
x nin T
;
contradiction
then A3:
ex
n being
Nat st
S1[
n]
by A2;
consider n being
Nat such that A4:
(
S1[
n] & ( for
m being
Nat st
S1[
m] holds
n <= m ) )
from NAT_1:sch 5(A3);
deffunc H1(
Nat)
-> Element of
S =
(iter (((curry' f) . I),($1 -' 1))) . s;
consider r being
FinSequence such that A5:
(
len r = n + 1 & ( for
k being
Nat st
k in dom r holds
r . k = H1(
k) ) )
from FINSEQ_1:sch 2();
rng r c= S
then reconsider r =
r as non
empty FinSequence of
S by A5, FINSEQ_1:def 4;
A8:
1
<= n + 1
by NAT_1:11;
then A9:
1
in dom r
by A5, FINSEQ_3:25;
A10:
n + 1
in dom r
by A5, A8, FINSEQ_3:25;
A11:
1
-' 1
= 0
by XREAL_1:232;
A12:
(n + 1) -' 1
= n
by NAT_D:34;
A13:
iter (
((curry' f) . I),
0)
= id S
by FUNCT_7:84;
r . 1
= H1(1)
by A5, A9;
then A14:
r . 1
= s
by A11, A13;
A15:
r . (len r) nin T
by A4, A5, A10, A12;
now for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) )let i be
Nat;
( 1 <= i & i < len r implies ( r . i in T & r . (i + 1) = f . ((r . i),I) ) )assume that A16:
1
<= i
and A17:
i < len r
;
( r . i in T & r . (i + 1) = f . ((r . i),I) )consider j being
Nat such that A18:
i = 1
+ j
by A16, NAT_1:10;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
A19:
i -' 1
= j
by A18, NAT_D:34;
A20:
(i + 1) -' 1
= i
by NAT_D:34;
A21:
dom (curry' f) = the
carrier of
A
by FUNCT_2:def 1;
dom ((curry' f) . I) = S
by FUNCT_2:def 1;
then A22:
((curry' f) . I) . ((iter (((curry' f) . I),j)) . s) = f . (
((iter (((curry' f) . I),j)) . s),
I)
by A21, FUNCT_5:34;
A23:
iter (
((curry' f) . I),
i)
= ((curry' f) . I) * (iter (((curry' f) . I),j))
by A18, FUNCT_7:71;
A24:
1
<= i + 1
by A16, NAT_1:13;
A25:
i + 1
<= n + 1
by A5, A17, NAT_1:13;
A26:
i -' 1
< n
by A5, A17, A18, A19, XREAL_1:6;
A27:
i in dom r
by A16, A17, FINSEQ_3:25;
A28:
i + 1
in dom r
by A5, A24, A25, FINSEQ_3:25;
A29:
r . i = (iter (((curry' f) . I),(i -' 1))) . s
by A5, A27;
r . (i + 1) = (iter (((curry' f) . I),i)) . s
by A5, A20, A28;
hence
(
r . i in T &
r . (i + 1) = f . (
(r . i),
I) )
by A4, A19, A22, A23, A26, A29, FUNCT_2:15;
verum end;
hence
contradiction
by A1, A14, A15;
verum
end;
end;
assume A30:
((curry' f) . I) orbit s c= T
; not f iteration_terminates_for I,s
given r being non empty FinSequence of S such that A31:
r . 1 = s
and
A32:
r . (len r) nin T
and
A33:
for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) )
; AOFA_000:def 33 contradiction
defpred S1[ Nat] means ( $1 + 1 <= len r implies r . ($1 + 1) in ((curry' f) . I) orbit s );
dom ((curry' f) . I) = S
by FUNCT_2:def 1;
then A34:
S1[ 0 ]
by A31, Th6;
A35:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A36:
S1[
i]
and A37:
(i + 1) + 1
<= len r
;
r . ((i + 1) + 1) in ((curry' f) . I) orbit s
A38:
1
<= i + 1
by NAT_1:11;
A39:
i + 1
< len r
by A37, NAT_1:13;
then
i + 1
in dom r
by A38, FINSEQ_3:25;
then A40:
r . (i + 1) in rng r
by FUNCT_1:3;
dom f = [:S, the carrier of A:]
by FUNCT_2:def 1;
then A41:
[(r . (i + 1)),I] in dom f
by A40, ZFMISC_1:87;
consider n being
Element of
NAT such that A42:
r . (i + 1) = (iter (((curry' f) . I),n)) . s
and
s in dom (iter (((curry' f) . I),n))
by A36, A37, NAT_1:13;
A43:
r . ((i + 1) + 1) =
f . (
(r . (i + 1)),
I)
by A33, A38, A39
.=
((curry' f) . I) . (r . (i + 1))
by A41, FUNCT_5:22
.=
(((curry' f) . I) * (iter (((curry' f) . I),n))) . s
by A42, FUNCT_2:15
.=
(iter (((curry' f) . I),(n + 1))) . s
by FUNCT_7:71
;
dom (iter (((curry' f) . I),(n + 1))) = S
by FUNCT_2:def 1;
hence
r . ((i + 1) + 1) in ((curry' f) . I) orbit s
by A43;
verum
end;
consider i being Nat such that
A44:
len r = i + 1
by NAT_1:6;
for n being Nat holds S1[n]
from NAT_1:sch 2(A34, A35);
then
r . (i + 1) in ((curry' f) . I) orbit s
by A44;
hence
contradiction
by A30, A32, A44; verum