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 Th37
.= DataPart ((StepWhile>0 (a,I,s2)) . (k + 1)) by A4, A5, A6, Th37 ;
:: 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, Def4;
A9: I is_halting_on (StepWhile>0 (a,I,s1)) . k by A1, A7, Def4;
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 ((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)))))) + 3))) by SCMFSA_9:def 5
.= 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 ((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)))))))) by A7, A8, A9, Th36 ;
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 ((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)))))) + 3))) by SCMFSA_9:def 5
.= 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 ((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)))))))) by A5, A7, A10, Th36 ;
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 ((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 ((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))))) 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 5
.= DataPart ((StepWhile>0 (a,I,s2)) . 0) by A2, SCMFSA_9:def 5 ;
then A17: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A17, A3); :: thesis: verum