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 & WithVariantWhile>0 a,Ig,s1 holds
WithVariantWhile>0 a,Ig,s2
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 & WithVariantWhile>0 a,Ig,s1 holds
WithVariantWhile>0 a,Ig,s2
let Ig be good Program of SCM+FSA ; :: thesis: ( s1 . (intloc 0 ) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1 & WithVariantWhile>0 a,Ig,s1 implies WithVariantWhile>0 a,Ig,s2 )
set I = Ig;
assume that
A1: s1 . (intloc 0 ) = 1 and
A2: DataPart s1 = DataPart s2 and
A3: ProperBodyWhile>0 a,Ig,s1 and
A4: WithVariantWhile>0 a,Ig,s1 ; :: thesis: WithVariantWhile>0 a,Ig,s2
set SW1 = StepWhile>0 a,Ig,s1;
set SW2 = StepWhile>0 a,Ig,s2;
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,s1) . (k + 1)) < f . ((StepWhile>0 a,Ig,s1) . k) or ((StepWhile>0 a,Ig,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,s2) . (k + 1)) < f . ((StepWhile>0 a,Ig,s2) . k) or ((StepWhile>0 a,Ig,s2) . k) . a <= 0 )
let k be Element of NAT ; :: thesis: ( f . ((StepWhile>0 a,Ig,s2) . (k + 1)) < f . ((StepWhile>0 a,Ig,s2) . k) or ((StepWhile>0 a,Ig,s2) . k) . a <= 0 )
A7: DataPart ((StepWhile>0 a,Ig,s1) . k) = DataPart ((StepWhile>0 a,Ig,s2) . k) by A2, A3, Th40;
then A8: ((StepWhile>0 a,Ig,s1) . k) . a = ((StepWhile>0 a,Ig,s2) . k) . a by SCMFSA6A:38;
DataPart ((StepWhile>0 a,Ig,s1) . (k + 1)) = DataPart ((StepWhile>0 a,Ig,s2) . (k + 1)) by A2, A3, Th40;
then ( f . ((StepWhile>0 a,Ig,s1) . k) = f . ((StepWhile>0 a,Ig,s2) . k) & f . ((StepWhile>0 a,Ig,s1) . (k + 1)) = f . ((StepWhile>0 a,Ig,s2) . (k + 1)) ) by A5, A7, Def7;
hence ( f . ((StepWhile>0 a,Ig,s2) . (k + 1)) < f . ((StepWhile>0 a,Ig,s2) . k) or ((StepWhile>0 a,Ig,s2) . k) . a <= 0 ) by A6, A8; :: thesis: verum