let s1, s2 be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st ProperBodyWhile=0 a,I,s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 a,I,s1) . k) = DataPart ((StepWhile=0 a,I,s2) . k)
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st ProperBodyWhile=0 a,I,s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 a,I,s1) . k) = DataPart ((StepWhile=0 a,I,s2) . k)
let I be Program of SCM+FSA ; :: thesis: ( ProperBodyWhile=0 a,I,s1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds DataPart ((StepWhile=0 a,I,s1) . k) = DataPart ((StepWhile=0 a,I,s2) . k) )
assume that
A1: ProperBodyWhile=0 a,I,s1 and
A2: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds DataPart ((StepWhile=0 a,I,s1) . k) = DataPart ((StepWhile=0 a,I,s2) . k)
set WH = while=0 a,I;
set ST2 = StepWhile=0 a,I,s2;
set ST1 = StepWhile=0 a,I,s1;
defpred S₁[ Nat] means DataPart ((StepWhile=0 a,I,s1) . $1) = DataPart ((StepWhile=0 a,I,s2) . $1);
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
set ST1kI = ((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA ));
set ST2kI = ((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA ));
assume A4: DataPart ((StepWhile=0 a,I,s1) . k) = DataPart ((StepWhile=0 a,I,s2) . k) ; :: thesis: S₁[k + 1]
then A5: ((StepWhile=0 a,I,s1) . k) . a = ((StepWhile=0 a,I,s2) . k) . a by SCMFSA6A:38;

per cases ( ((StepWhile=0 a,I,s1) . k) . a <> 0 or ((StepWhile=0 a,I,s1) . k) . a = 0 ) ;

suppose A6: ((StepWhile=0 a,I,s1) . k) . a <> 0 ; :: thesis: S₁[k + 1]

hence DataPart ((StepWhile=0 a,I,s1) . (k + 1)) = DataPart ((StepWhile=0 a,I,s1) . k) by Th24
.= DataPart ((StepWhile=0 a,I,s2) . (k + 1)) by A4, A5, A6, Th24 ;
:: thesis: verum

end;

suppose A7: ((StepWhile=0 a,I,s1) . k) . a = 0 ; :: thesis: S₁[k + 1]

then A8: I is_closed_on (StepWhile=0 a,I,s1) . k by A1, Def1;
A9: I is_halting_on (StepWhile=0 a,I,s1) . k by A1, A7, Def1;
then A10: ( I is_closed_on (StepWhile=0 a,I,s2) . k & I is_halting_on (StepWhile=0 a,I,s2) . k ) by A4, A8, SCMFSA8B:8;
A11: DataPart ((StepWhile=0 a,I,s1) . (k + 1)) = DataPart (Comput (ProgramPart (((StepWhile=0 a,I,s1) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s1) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) by SCMFSA_9:def 4
.= DataPart (Comput (ProgramPart (((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA ))))) by A7, A8, A9, Th23 ;
A12: DataPart ((StepWhile=0 a,I,s2) . (k + 1)) = DataPart (Comput (ProgramPart (((StepWhile=0 a,I,s2) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s2) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) by SCMFSA_9:def 4
.= DataPart (Comput (ProgramPart (((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA )))),(((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA ))))) by A5, A7, A10, Th23 ;
A13: ( I +* (Start-At 0 ,SCM+FSA ) c= ((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA )) & I +* (Start-At 0 ,SCM+FSA ) c= ((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA )) ) by FUNCT_4:26;
A14: DataPart ((StepWhile=0 a,I,s1) . k) = DataPart (((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
then A15: I is_closed_on ((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA )) by A8, SCMFSA8B:6;
A16: DataPart (((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA ))) = DataPart ((StepWhile=0 a,I,s1) . k) by SCMFSA8A:11
.= DataPart (((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA ))) by A4, SCMFSA8A:11 ;
I is_halting_on ((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA )) by A8, A9, A14, SCMFSA8B:8;
then LifeSpan (((StepWhile=0 a,I,s1) . k) +* (I +* (Start-At 0 ,SCM+FSA ))) = LifeSpan (((StepWhile=0 a,I,s2) . k) +* (I +* (Start-At 0 ,SCM+FSA ))) by A8, A16, A13, A14, SCMFSA8B:6, SCMFSA8C:44;
hence S₁[k + 1] by A11, A12, A16, A13, A15, SCMFSA8C:43; :: thesis: verum

end;

end;

end;

DataPart ((StepWhile=0 a,I,s1) . 0 ) = DataPart s1 by SCMFSA_9:def 4
.= DataPart ((StepWhile=0 a,I,s2) . 0 ) by A2, SCMFSA_9:def 4 ;
then A17: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A17, A3); :: thesis: verum