let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for l being Nat
for P being NAT -defined the InstructionsF 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 with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for l being Nat
for P being NAT -defined the InstructionsF 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 Nat; :: thesis: for P being NAT -defined the InstructionsF 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 InstructionsF 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 A4: Start-At (l,S) c= s by A2, XBOOLE_1:1;
A5: l .--> (halt S) c= Q by A1, A3, XBOOLE_1:1;
IC in dom (Start-At (l,S)) by MEMSTR_0:15;
then A7: IC s = IC (Start-At (l,S)) by A4, GRFUNC_1:2
.= l by FUNCOP_1:72 ;
A8: IC s in dom (l .--> (halt S)) by A7, TARSKI:def 1;
A9: dom (l .--> (halt S)) c= dom Q by A5, RELAT_1:11;
thus CurInstr (Q,(Comput (Q,s,0))) = CurInstr (Q,s)
.= Q . (IC s) by A9, A8, PARTFUN1:def 6
.= (l .--> (halt S)) . (IC s) by A8, A5, GRFUNC_1:2
.= CurInstr ((l .--> (halt S)),s) by A8, PARTFUN1:def 6
.= halt S by A4, A5, Th9 ; :: thesis: verum