let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated 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 holds p is P -halted
let S be non empty IC-Ins-separated 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 holds p is P -halted
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 holds p is P -halted
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 holds p is P -halted )
assume A1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S holds p is P -halted
let p be l -started PartState of S; :: thesis: p is P -halted
set h = halt S;
set I = p +* P;
let s be State of S; :: according to EXTPRO_1:def 11 :: thesis: ( p c= s implies for P being Instruction-Sequence of S st P c= P holds
P halts_on s )
assume A2: p c= s ; :: thesis: for P being Instruction-Sequence of S st P c= P holds
P halts_on s
let Q be Instruction-Sequence of S; :: thesis: ( P c= Q implies Q halts_on s )
assume A3: P c= Q ; :: thesis: Q halts_on s
take 0 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (Q,s,0)) in dom Q & CurInstr (Q,(Comput (Q,s,0))) = halt S )
dom Q = NAT by PARTFUN1:def 2;
hence IC (Comput (Q,s,0)) in dom Q ; :: thesis: CurInstr (Q,(Comput (Q,s,0))) = halt S
Start-At (l,S) c= p by MEMSTR_0:29;
then A5: Start-At (l,S) c= s by A2, XBOOLE_1:1;
A6: l .--> (halt S) c= Q by A1, A3, XBOOLE_1:1;
A7: dom (l .--> (halt S)) = {l} by FUNCOP_1:13;
IC in dom (Start-At (l,S)) by MEMSTR_0:15;
then A8: IC s = IC (Start-At (l,S)) by A5, GRFUNC_1:2
.= l by FUNCOP_1:72 ;
A9: IC s in dom (l .--> (halt S)) by A7, A8, TARSKI:def 1;
A10: dom (l .--> (halt S)) c= dom Q by A6, RELAT_1:11;
thus CurInstr (Q,(Comput (Q,s,0))) = CurInstr (Q,s) by Th3
.= Q . (IC s) by A10, A9, PARTFUN1:def 6
.= (l .--> (halt S)) . (IC s) by A9, A6, GRFUNC_1:2
.= CurInstr ((l .--> (halt S)),s) by A9, PARTFUN1:def 6
.= halt S by A5, Th10 ; :: thesis: verum