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 Program 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 Program 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 Program 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 Program 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 Object-Kind of SCM+FSA),NAT such that
A5: f is on_data_only and
A6: for k being Element of 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, Th46;
take f ; :: according to SCMFSA9A:def 5 :: thesis: for k being Element of 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 Element of 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, Th40;
then A7: f . ((StepWhile>0 (a,Ig,p1,s1)) . (k + 1)) = f . ((StepWhile>0 (a,Ig,p2,s2)) . (k + 1)) by A5, Def7;
A8: DataPart ((StepWhile>0 (a,Ig,p1,s1)) . k) = DataPart ((StepWhile>0 (a,Ig,p2,s2)) . k) by A2, A3, Th40;
then A9: ((StepWhile>0 (a,Ig,p1,s1)) . k) . a = ((StepWhile>0 (a,Ig,p2,s2)) . k) . a by SCMFSA6A:7;
f . ((StepWhile>0 (a,Ig,p1,s1)) . k) = f . ((StepWhile>0 (a,Ig,p2,s2)) . k) by A5, A8, Def7;
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