let s1, s2 be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1 holds
ProperBodyWhile>0 a,I,s2
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1 holds
ProperBodyWhile>0 a,I,s2
let I be Program of SCM+FSA ; :: thesis: ( DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1 implies ProperBodyWhile>0 a,I,s2 )
assume that
A1: DataPart s1 = DataPart s2 and
A2: ProperBodyWhile>0 a,I,s1 ; :: thesis: ProperBodyWhile>0 a,I,s2
let k be Element of NAT ; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 a,I,s2) . k) . a > 0 implies ( I is_closed_on (StepWhile>0 a,I,s2) . k & I is_halting_on (StepWhile>0 a,I,s2) . k ) )
assume A3: ((StepWhile>0 a,I,s2) . k) . a > 0 ; :: thesis: ( I is_closed_on (StepWhile>0 a,I,s2) . k & I is_halting_on (StepWhile>0 a,I,s2) . k )
A4: DataPart ((StepWhile>0 a,I,s2) . k) = DataPart ((StepWhile>0 a,I,s1) . k) by A1, A2, Th40;
then ((StepWhile>0 a,I,s1) . k) . a > 0 by A3, SCMFSA6A:38;
then ( I is_closed_on (StepWhile>0 a,I,s1) . k & I is_halting_on (StepWhile>0 a,I,s1) . k ) by A2, Def4;
hence ( I is_closed_on (StepWhile>0 a,I,s2) . k & I is_halting_on (StepWhile>0 a,I,s2) . k ) by A4, SCMFSA8B:8; :: thesis: verum