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 really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being 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 really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being 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 really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: ( ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 implies for k being 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 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));
defpred S₁[ Nat] means DataPart ((StepWhile=0 (a,I,p1,s1)) . $1) = DataPart ((StepWhile=0 (a,I,p2,s2)) . $1);
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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;
A4: I c= (p1 +* (while=0 (a,I))) +* I by FUNCT_4:25;
A5: I c= (p2 +* (while=0 (a,I))) +* I by FUNCT_4:25;
assume A6: DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k) ; :: thesis: S₁[k + 1]
then A7: ((StepWhile=0 (a,I,p1,s1)) . k) . a = ((StepWhile=0 (a,I,p2,s2)) . k) . a by SCMFSA_M:2;

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

suppose A8: ((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 Th18
.= DataPart ((StepWhile=0 (a,I,p2,s2)) . (k + 1)) by A6, A7, A8, Th18 ;
:: thesis: verum

end;

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

A10: I is_halting_on (StepWhile=0 (a,I,p1,s1)) . k,p1 +* (while=0 (a,I)) by A1, A9;
then A11: I is_halting_on (StepWhile=0 (a,I,p2,s2)) . k,p2 +* (while=0 (a,I)) by A6, SCMFSA8B:5;
A12: 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)))) + 2))) by 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 A9, A10, Th17 ;
A13: 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)))) + 2))) by 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 A7, A9, A11, Th17 ;
A14: DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart (Initialize ((StepWhile=0 (a,I,p1,s1)) . k)) by MEMSTR_0:79;
A15: 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 A6, MEMSTR_0:79 ;
I is_halting_on Initialize ((StepWhile=0 (a,I,p1,s1)) . k),(p1 +* (while=0 (a,I))) +* I by A10, A14, 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 A15, A4, A5, SCMFSA8C:18;
hence S₁[k + 1] by A12, A13, A15, A4, A5, 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 A16: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A16, A3); :: thesis: verum