let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for Ig being good Program of SCM+FSA st s . (intloc 0 ) = 1 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s holds
ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
( f is on_data_only & ( for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )
let a be read-write Int-Location ; :: thesis: for Ig being good Program of SCM+FSA st s . (intloc 0 ) = 1 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s holds
ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
( f is on_data_only & ( for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )
let Ig be good Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s implies ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
( f is on_data_only & ( for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) ) )
set I = Ig;
assume that
A1: s . (intloc 0 ) = 1 and
A2: ProperBodyWhile>0 a,Ig,s and
A3: WithVariantWhile>0 a,Ig,s ; :: thesis: ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
( f is on_data_only & ( for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )
set SW = StepWhile>0 a,Ig,s;
consider g being Function of (product the Object-Kind of SCM+FSA ),NAT such that
A4: for k being Element of NAT holds
( g . ((StepWhile>0 a,Ig,s) . (k + 1)) < g . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) by A3, Def5;
consider K being Element of NAT such that
A5: ExitsAtWhile>0 a,Ig,s = K and
A6: ((StepWhile>0 a,Ig,s) . K) . a <= 0 and
for i being Element of NAT st ((StepWhile>0 a,Ig,s) . i) . a <= 0 holds
K <= i and
DataPart (Computation (s +* ((while>0 a,Ig) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,Ig) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,Ig,s) . K) by A2, A3, Def6;
defpred S₁[ State of SCM+FSA , set ] means ( ex k being Element of NAT st
( k <= K & DataPart $1 = DataPart ((StepWhile>0 a,Ig,s) . k) & $2 = g . ((StepWhile>0 a,Ig,s) . k) ) or ( ( for k being Element of NAT holds
( not k <= K or not DataPart $1 = DataPart ((StepWhile>0 a,Ig,s) . k) ) ) & $2 = 0 ) );
A7: for x being State of SCM+FSA ex y being Element of NAT st S₁[x,y]

proof

let x be State of SCM+FSA ; :: thesis: ex y being Element of NAT st S₁[x,y]

per cases ( ex k being Element of NAT st
( k <= K & DataPart x = DataPart ((StepWhile>0 a,Ig,s) . k) ) or for k being Element of NAT holds
( not k <= K or not DataPart x = DataPart ((StepWhile>0 a,Ig,s) . k) ) ) ;

suppose ex k being Element of NAT st
( k <= K & DataPart x = DataPart ((StepWhile>0 a,Ig,s) . k) ) ; :: thesis: ex y being Element of NAT st S₁[x,y]

then consider k being Element of NAT such that
A8: ( k <= K & DataPart x = DataPart ((StepWhile>0 a,Ig,s) . k) ) ;
take g . ((StepWhile>0 a,Ig,s) . k) ; :: thesis: S₁[x,g . ((StepWhile>0 a,Ig,s) . k)]
thus S₁[x,g . ((StepWhile>0 a,Ig,s) . k)] by A8; :: thesis: verum

end;

suppose A9: for k being Element of NAT holds
( not k <= K or not DataPart x = DataPart ((StepWhile>0 a,Ig,s) . k) ) ; :: thesis: ex y being Element of NAT st S₁[x,y]

take 0 ; :: thesis: S₁[x, 0 ]
thus S₁[x, 0 ] by A9; :: thesis: verum

end;

end;

end;

consider f being Function of (product the Object-Kind of SCM+FSA ),NAT such that
A10: for x being State of SCM+FSA holds S₁[x,f . x] from FUNCT_2:sch 3(A7);
take f ; :: thesis: ( f is on_data_only & ( for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )

hereby :: according to SCMFSA9A:def 7 :: thesis: for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 )

let s1, s2 be State of SCM+FSA ; :: thesis: ( DataPart s1 = DataPart s2 implies f . s1 = f . s2 )
assume A11: DataPart s1 = DataPart s2 ; :: thesis: f . s1 = f . s2
( S₁[s1,f . s1] & S₁[s2,f . s2] ) by A10;
hence f . s1 = f . s2 by A1, A2, A3, A5, A11, Th45; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 )

per cases ( k < K or K <= k ) ;

suppose A12: k < K ; :: thesis: ( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 )

then A13: k + 1 <= K by NAT_1:13;
consider kk being Element of NAT such that
A14: ( kk <= K & DataPart ((StepWhile>0 a,Ig,s) . k) = DataPart ((StepWhile>0 a,Ig,s) . kk) & f . ((StepWhile>0 a,Ig,s) . k) = g . ((StepWhile>0 a,Ig,s) . kk) ) by A10, A12;
consider kk1 being Element of NAT such that
A15: ( kk1 <= K & DataPart ((StepWhile>0 a,Ig,s) . (k + 1)) = DataPart ((StepWhile>0 a,Ig,s) . kk1) & f . ((StepWhile>0 a,Ig,s) . (k + 1)) = g . ((StepWhile>0 a,Ig,s) . kk1) ) by A10, A13;
( k = kk & k + 1 = kk1 ) by A1, A2, A3, A5, A12, A13, A14, A15, Th45;
hence ( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) by A4, A14, A15; :: thesis: verum

end;

suppose K <= k ; :: thesis: ( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 )

then DataPart ((StepWhile>0 a,Ig,s) . K) = DataPart ((StepWhile>0 a,Ig,s) . k) by A6, Th43;
hence ( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) by A6, SCMFSA6A:38; :: thesis: verum

end;

end;