let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for l being Element of NAT
for P being NAT -defined the Instructions of b₁ -valued Function st l .--> (halt S) c= P holds
for p being b₂ -started PartState of S
for s being State of S st p +* P c= s holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N; :: thesis: for l being Element of NAT
for P being NAT -defined the Instructions of S -valued Function st l .--> (halt S) c= P holds
for p being b₁ -started PartState of S
for s being State of S st p +* P c= s holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s
let l be Element of NAT ; :: thesis: for P being NAT -defined the Instructions of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S
for s being State of S st p +* P c= s holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s
let P be NAT -defined the Instructions of S -valued Function; :: thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S
for s being State of S st p +* P c= s holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s )
assume Z1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S
for s being State of S st p +* P c= s holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s
let p be l -started PartState of S; :: thesis: for s being State of S st p +* P c= s holds
for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s
let s be State of S; :: thesis: ( p +* P c= s implies for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s )
assume A3: p +* P c= s ; :: thesis: for i being Element of NAT holds Comput ((ProgramPart s),s,i) = s
AA: Start-At (l,S) c= p by COMPOS_1:151;
defpred S₁[ Element of NAT ] means Comput ((ProgramPart s),s,$1) = s;
dom (Start-At (l,S)) misses dom P by COMPOS_1:130;
then Start-At (l,S) c= p +* P by AA, FUNCT_4:125;
then B3: Start-At (l,S) c= s by A3, XBOOLE_1:1;

A4: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
P c= p +* P by FUNCT_4:26;
then P c= s by A3, XBOOLE_1:1;
then B5: l .--> (halt S) c= s by Z1, XBOOLE_1:1;
Comput ((ProgramPart s),s,(i + 1)) = Following ((ProgramPart s),s) by A5, Th14
.= Exec ((halt S),s) by B3, B5, COMPOS_1:6, RELAT_1:210
.= s by Def8 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ] by Th3;
thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A6, A4); :: thesis: verum