let A be preIfWhileAlgebra; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )
set g = (curry' f) . I;

hereby :: thesis: ( ((curry' f) . I) orbit s c= T implies not f iteration_terminates_for I,s )

assume A1: not f iteration_terminates_for I,s ; :: thesis: ((curry' f) . I) orbit s c= T
thus ((curry' f) . I) orbit s c= T :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin ((curry' f) . I) orbit s or not x nin T )
assume x in ((curry' f) . I) orbit s ; :: thesis: 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 S₁[ Nat] means (iter (((curry' f) . I),$1)) . s nin T;
assume x nin T ; :: thesis: contradiction
then A3: ex n being Nat st S₁[n] by A2;
consider n being Nat such that
A4: ( S₁[n] & ( for m being Nat st S₁[m] holds
n <= m ) ) from NAT_1:sch 5(A3);
deffunc H₁( 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 = H₁(k) ) ) from FINSEQ_1:sch 2();
rng r c= S

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( a nin rng r or not a nin S )
assume a in rng r ; :: thesis: not a nin S
then consider b being object such that
A6: b in dom r and
A7: a = r . b by FUNCT_1:def 3;
reconsider b = b as Element of NAT by A6;
r . b = (iter (((curry' f) . I),(b -' 1))) . s by A5, A6;
hence not a nin S by A7; :: thesis: verum

end;

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 = H₁(1) by A5, A9;
then A14: r . 1 = s by A11, A13;
A15: r . (len r) nin T by A4, A5, A10, A12;

now :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;

hence contradiction by A1, A14, A15; :: thesis: verum

end;

end;

assume A30: ((curry' f) . I) orbit s c= T ; :: thesis: 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) ) ; :: according to AOFA_000:def 33 :: thesis: contradiction
defpred S₁[ 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: S₁[ 0 ] by A31, Th6;
A35: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A36: S₁[i] and
A37: (i + 1) + 1 <= len r ; :: thesis: 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; :: thesis: verum

end;

consider i being Nat such that
A44: len r = i + 1 by NAT_1:6;
for n being Nat holds S₁[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; :: thesis: verum