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 I being Program of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
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,p1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
let I be Program of SCM+FSA; :: thesis: ( ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k) )
assume that
A1: ProperBodyWhile=0 a,I,s1,p1 and
A2: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
set WH = while=0 (a,I);
set ST2 = StepWhile=0 (a,I,p2,s2);
set PT2 = p2 +* (while=0 (a,I));
set ST1 = StepWhile=0 (a,I,p1,s1);
set PT1 = p1 +* (while=0 (a,I));
A3: (p2 +* (while=0 (a,I))) +* (while=0 (a,I)) = p2 +* (while=0 (a,I)) by FUNCT_4:93;
A4: (p1 +* (while=0 (a,I))) +* (while=0 (a,I)) = p1 +* (while=0 (a,I)) by FUNCT_4:93;
defpred S₁[ Nat] means DataPart ((StepWhile=0 (a,I,p1,s1)) . $1) = DataPart ((StepWhile=0 (a,I,p2,s2)) . $1);
A5: 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 = Initialize ((StepWhile=0 (a,I,p1,s1)) . k);
set PT1I = (p1 +* (while=0 (a,I))) +* I;
set ST2kI = Initialize ((StepWhile=0 (a,I,p2,s2)) . k);
set PT2I = (p2 +* (while=0 (a,I))) +* I;
A6: I c= (p1 +* (while=0 (a,I))) +* I by FUNCT_4:25;
A7: I c= (p2 +* (while=0 (a,I))) +* I by FUNCT_4:25;
assume A8: DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k) ; :: thesis: S₁[k + 1]
then A9: ((StepWhile=0 (a,I,p1,s1)) . k) . a = ((StepWhile=0 (a,I,p2,s2)) . k) . a by SCMFSA6A:7;

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

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

hence DataPart ((StepWhile=0 (a,I,p1,s1)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p1,s1)) . k) by Th24
.= DataPart ((StepWhile=0 (a,I,p2,s2)) . (k + 1)) by A8, A9, A10, Th24 ;
:: thesis: verum

end;

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

then A12: I is_closed_on (StepWhile=0 (a,I,p1,s1)) . k,p1 +* (while=0 (a,I)) by A1, Def1;
A13: I is_halting_on (StepWhile=0 (a,I,p1,s1)) . k,p1 +* (while=0 (a,I)) by A1, A11, Def1;
then A14: ( I is_closed_on (StepWhile=0 (a,I,p2,s2)) . k,p2 +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p2,s2)) . k,p2 +* (while=0 (a,I)) ) by A8, A12, SCMFSA8B:5;
A15: DataPart ((StepWhile=0 (a,I,p1,s1)) . (k + 1)) = DataPart (Comput (((p1 +* (while=0 (a,I))) +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,p1,s1)) . k)),((LifeSpan (((p1 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p1,s1)) . k)))) + 3))) by A4, SCMFSA_9:def 4
.= DataPart (Comput (((p1 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p1,s1)) . k)),(LifeSpan (((p1 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p1,s1)) . k)))))) by A11, A12, A13, Th23 ;
A16: DataPart ((StepWhile=0 (a,I,p2,s2)) . (k + 1)) = DataPart (Comput (((p2 +* (while=0 (a,I))) +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,p2,s2)) . k)),((LifeSpan (((p2 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p2,s2)) . k)))) + 3))) by A3, SCMFSA_9:def 4
.= DataPart (Comput (((p2 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p2,s2)) . k)),(LifeSpan (((p2 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p2,s2)) . k)))))) by A9, A11, A14, Th23 ;
A18: DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart (Initialize ((StepWhile=0 (a,I,p1,s1)) . k)) by MEMSTR_0:79;
then A19: I is_closed_on Initialize ((StepWhile=0 (a,I,p1,s1)) . k),(p1 +* (while=0 (a,I))) +* I by A12, SCMFSA8B:3;
A20: DataPart (Initialize ((StepWhile=0 (a,I,p1,s1)) . k)) = DataPart ((StepWhile=0 (a,I,p1,s1)) . k) by MEMSTR_0:79
.= DataPart (Initialize ((StepWhile=0 (a,I,p2,s2)) . k)) by A8, MEMSTR_0:79 ;
I is_halting_on Initialize ((StepWhile=0 (a,I,p1,s1)) . k),(p1 +* (while=0 (a,I))) +* I by A12, A13, A18, SCMFSA8B:5;
then LifeSpan (((p1 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p1,s1)) . k))) = LifeSpan (((p2 +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p2,s2)) . k))) by A12, A20, A18, A6, A7, SCMFSA8B:3, SCMFSA8C:18;
hence S₁[k + 1] by A15, A16, A20, A19, A6, A7, SCMFSA8C:17; :: thesis: verum

end;

end;

end;

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