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_{1} -valued Function st l .--> (halt S) c= P holds

for p being b_{2} -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_{1} -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

for l being Nat

for P being NAT -defined the InstructionsF of b

for p being b

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

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