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

proof

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

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

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

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

end;

suppose A9: for k being Nat holds
( not k <= K or not DataPart x = DataPart ((StepWhile>0 (a,Ig,p,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_Values_of SCM+FSA)),NAT such that
A10: for x being Element of product (the_Values_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 Nat holds
( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) ) )

hereby :: according to MEMSTR_0:def 18 :: thesis: for k being Nat holds
( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,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
reconsider ss1 = s1, ss2 = s2 as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
( S₁[ss1,f . ss1] & S₁[ss2,f . ss2] ) by A10;
hence f . s1 = f . s2 by A1, A2, A3, A4, A11, Th39; :: thesis: verum

end;

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

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

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

then A13: k + 1 <= K by NAT_1:13;
then consider kk1 being Nat such that
A14: ( kk1 <= K & DataPart ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,Ig,p,s)) . kk1) ) and
A15: f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) = g . ((StepWhile>0 (a,Ig,p,s)) . kk1) by A10;
A16: k + 1 = kk1 by A1, A2, A3, A4, A13, A14, Th39;
consider kk being Nat such that
A17: ( kk <= K & DataPart ((StepWhile>0 (a,Ig,p,s)) . k) = DataPart ((StepWhile>0 (a,Ig,p,s)) . kk) ) and
A18: f . ((StepWhile>0 (a,Ig,p,s)) . k) = g . ((StepWhile>0 (a,Ig,p,s)) . kk) by A10, A12;
k = kk by A1, A2, A3, A4, A12, A17, Th39;
hence ( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) by A6, A18, A15, A16; :: thesis: verum

end;

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

then DataPart ((StepWhile>0 (a,Ig,p,s)) . K) = DataPart ((StepWhile>0 (a,Ig,p,s)) . k) by A5, Th37;
hence ( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) by A5, SCMFSA_M:2; :: thesis: verum

end;

end;