let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
let a be read-write Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
let I be MacroInstruction of SCM+FSA ; :: thesis: for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
let k be Nat; :: thesis: ( ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 implies for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )
set SW = StepWhile>0 (a,I,p,s);
set PW = p +* (while>0 (a,I));
defpred S₁[ Nat] means ( k <= $1 implies DataPart ((StepWhile>0 (a,I,p,s)) . $1) = DataPart ((StepWhile>0 (a,I,p,s)) . k) );
assume A1: ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ; :: thesis: for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

assume A4: k <= n + 1 ; :: thesis: DataPart ((StepWhile>0 (a,I,p,s)) . (n + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

per cases ( k <= n or k = n + 1 ) by A4, NAT_1:8;

suppose A5: k <= n ; :: thesis: DataPart ((StepWhile>0 (a,I,p,s)) . (n + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

then ((StepWhile>0 (a,I,p,s)) . n) . a <= 0 by A1, A3, SCMFSA_M:2;
hence DataPart ((StepWhile>0 (a,I,p,s)) . (n + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k) by A3, A5, Th31; :: thesis: verum

end;

suppose k = n + 1 ; :: thesis: DataPart ((StepWhile>0 (a,I,p,s)) . (n + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

hence DataPart ((StepWhile>0 (a,I,p,s)) . (n + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ; :: thesis: verum

end;

end;

end;

end;

A6: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A2); :: thesis: verum