let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 holds
WithVariantWhile>0 a,Ig,s2,p2
let s1, s2 be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 holds
WithVariantWhile>0 a,Ig,s2,p2
let a be read-write Int-Location; :: thesis: for Ig being good really-closed MacroInstruction of SCM+FSA st s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 holds
WithVariantWhile>0 a,Ig,s2,p2
let Ig be good really-closed MacroInstruction of SCM+FSA ; :: thesis: ( s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 implies WithVariantWhile>0 a,Ig,s2,p2 )
set I = Ig;
assume that
A1: s1 . (intloc 0) = 1 and
A2: DataPart s1 = DataPart s2 and
A3: ProperBodyWhile>0 a,Ig,s1,p1 and
A4: WithVariantWhile>0 a,Ig,s1,p1 ; :: thesis: WithVariantWhile>0 a,Ig,s2,p2
set SW1 = StepWhile>0 (a,Ig,p1,s1);
consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that
A5: f is on_data_only and
A6: for k being Nat holds
( f . ((StepWhile>0 (a,Ig,p1,s1)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p1,s1)) . k) or ((StepWhile>0 (a,Ig,p1,s1)) . k) . a <= 0 ) by A1, A3, A4, Th40;
take f ; :: according to SCMFSA9A:def 5 :: thesis: for k being Nat holds
( f . ((StepWhile>0 (a,Ig,p2,s2)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p2,s2)) . k) or ((StepWhile>0 (a,Ig,p2,s2)) . k) . a <= 0 )
let k be Nat; :: thesis: ( f . ((StepWhile>0 (a,Ig,p2,s2)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p2,s2)) . k) or ((StepWhile>0 (a,Ig,p2,s2)) . k) . a <= 0 )
set SW2 = StepWhile>0 (a,Ig,p2,s2);
DataPart ((StepWhile>0 (a,Ig,p1,s1)) . (k + 1)) = DataPart ((StepWhile>0 (a,Ig,p2,s2)) . (k + 1)) by A2, A3, Th34;
then A7: f . ((StepWhile>0 (a,Ig,p1,s1)) . (k + 1)) = f . ((StepWhile>0 (a,Ig,p2,s2)) . (k + 1)) by A5;
A8: DataPart ((StepWhile>0 (a,Ig,p1,s1)) . k) = DataPart ((StepWhile>0 (a,Ig,p2,s2)) . k) by A2, A3, Th34;
then A9: ((StepWhile>0 (a,Ig,p1,s1)) . k) . a = ((StepWhile>0 (a,Ig,p2,s2)) . k) . a by SCMFSA_M:2;
f . ((StepWhile>0 (a,Ig,p1,s1)) . k) = f . ((StepWhile>0 (a,Ig,p2,s2)) . k) by A5, A8;
hence ( f . ((StepWhile>0 (a,Ig,p2,s2)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p2,s2)) . k) or ((StepWhile>0 (a,Ig,p2,s2)) . k) . a <= 0 ) by A6, A9, A7; :: thesis: verum