let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)

let s be 0 -started State of SCMPDS; :: thesis: for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)

let i be parahalting Instruction of SCMPDS; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

set Li = Load i;

set Mi = Macro i;

set PI = P +* (Macro i);

set IC1 = IC (Comput ((P +* (Macro i)),s,1));

A1: Initialize s = s by MEMSTR_0:44;

Macro i c= P +* (Macro i) by FUNCT_4:25;

then A2: P +* (Macro i) halts_on s by SCMPDS_4:def 7;

A3: 1 in dom (Macro i) by COMPOS_1:57;

A4: 0 in dom (Macro i) by COMPOS_1:57;

A5: (Macro i) . 1 = halt SCMPDS by COMPOS_1:59;

A6: (Macro i) . 0 = i by COMPOS_1:58;

A7: Macro i c= P +* (Macro i) by FUNCT_4:25;

then A8: IC (Comput ((P +* (Macro i)),s,1)) in dom (Macro i) by SCMPDS_4:def 6;

A9: (P +* (Macro i)) /. (IC s) = (P +* (Macro i)) . (IC s) by PBOOLE:143;

A10: Comput ((P +* (Macro i)),s,(0 + 1)) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by EXTPRO_1:3

.= Following ((P +* (Macro i)),s)

.= Exec (((P +* (Macro i)) . 0),s) by A9, A1, MEMSTR_0:47

.= Exec (i,s) by A4, A6, A7, GRFUNC_1:2 ;

for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)

let s be 0 -started State of SCMPDS; :: thesis: for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)

let i be parahalting Instruction of SCMPDS; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

set Li = Load i;

set Mi = Macro i;

set PI = P +* (Macro i);

set IC1 = IC (Comput ((P +* (Macro i)),s,1));

A1: Initialize s = s by MEMSTR_0:44;

Macro i c= P +* (Macro i) by FUNCT_4:25;

then A2: P +* (Macro i) halts_on s by SCMPDS_4:def 7;

A3: 1 in dom (Macro i) by COMPOS_1:57;

A4: 0 in dom (Macro i) by COMPOS_1:57;

A5: (Macro i) . 1 = halt SCMPDS by COMPOS_1:59;

A6: (Macro i) . 0 = i by COMPOS_1:58;

A7: Macro i c= P +* (Macro i) by FUNCT_4:25;

then A8: IC (Comput ((P +* (Macro i)),s,1)) in dom (Macro i) by SCMPDS_4:def 6;

A9: (P +* (Macro i)) /. (IC s) = (P +* (Macro i)) . (IC s) by PBOOLE:143;

A10: Comput ((P +* (Macro i)),s,(0 + 1)) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by EXTPRO_1:3

.= Following ((P +* (Macro i)),s)

.= Exec (((P +* (Macro i)) . 0),s) by A9, A1, MEMSTR_0:47

.= Exec (i,s) by A4, A6, A7, GRFUNC_1:2 ;

per cases
( IC (Comput ((P +* (Macro i)),s,1)) = 0 or IC (Comput ((P +* (Macro i)),s,1)) = 1 )
by A8, COMPOS_1:60;

end;

suppose A11:
IC (Comput ((P +* (Macro i)),s,1)) = 0
; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

set Ni = InsCode i;

(IC s) + 1 = 0 + 1 by A1, MEMSTR_0:47;

then A12: InsCode i in {0,1,4,5,6,14} by A10, A11, SCMPDS_4:1;

A13: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) = (P +* (Macro i)) . 0 by A11, PBOOLE:143

.= i by A4, A6, A7, GRFUNC_1:2 ;

A14: InsCode i <> 1 by Th10;

end;(IC s) + 1 = 0 + 1 by A1, MEMSTR_0:47;

then A12: InsCode i in {0,1,4,5,6,14} by A10, A11, SCMPDS_4:1;

A13: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) = (P +* (Macro i)) . 0 by A11, PBOOLE:143

.= i by A4, A6, A7, GRFUNC_1:2 ;

A14: InsCode i <> 1 by Th10;

hereby :: thesis: verum
end;

per cases
( i = halt SCMPDS or i <> halt SCMPDS )
;

end;

suppose A15:
i <> halt SCMPDS
; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

.= Exec (i,s) by A10, EXTPRO_1:3 ;

A18: IC s = IC (Exec (i,s)) by A10, A11, A1, MEMSTR_0:47;

then A19: s = Exec (i,s) by A16, SCMPDS_2:44;

hence Exec (i,s) = IExec ((Load i),P,s) by A7, SCMPDS_4:def 7; :: thesis: verum

end;

A16: now :: thesis: for b being Int_position holds s . b = (Exec (i,s)) . b

A17: Following ((P +* (Macro i)),s) =
Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0)))
let b be Int_position; :: thesis: s . b_{1} = (Exec (i,s)) . b_{1}

end;per cases
( InsCode i = 0 or InsCode i = 14 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 )
by A12, A14, ENUMSET1:def 4;

end;

suppose
InsCode i = 14
; :: thesis: s . b_{1} = (Exec (i,s)) . b_{1}

then
ex k1 being Integer st i = goto k1
by SCMPDS_2:26;

hence s . b = (Exec (i,s)) . b by SCMPDS_2:54; :: thesis: verum

end;hence s . b = (Exec (i,s)) . b by SCMPDS_2:54; :: thesis: verum

suppose
InsCode i = 4
; :: thesis: s . b_{1} = (Exec (i,s)) . b_{1}

then
ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <>0_goto k2
by SCMPDS_2:30;

hence s . b = (Exec (i,s)) . b by SCMPDS_2:55; :: thesis: verum

end;hence s . b = (Exec (i,s)) . b by SCMPDS_2:55; :: thesis: verum

suppose
InsCode i = 5
; :: thesis: s . b_{1} = (Exec (i,s)) . b_{1}

then
ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <=0_goto k2
by SCMPDS_2:31;

hence s . b = (Exec (i,s)) . b by SCMPDS_2:56; :: thesis: verum

end;hence s . b = (Exec (i,s)) . b by SCMPDS_2:56; :: thesis: verum

suppose
InsCode i = 6
; :: thesis: s . b_{1} = (Exec (i,s)) . b_{1}

then
ex a being Int_position ex k1, k2 being Integer st i = (a,k1) >=0_goto k2
by SCMPDS_2:32;

hence s . b = (Exec (i,s)) . b by SCMPDS_2:57; :: thesis: verum

end;hence s . b = (Exec (i,s)) . b by SCMPDS_2:57; :: thesis: verum

.= Exec (i,s) by A10, EXTPRO_1:3 ;

A18: IC s = IC (Exec (i,s)) by A10, A11, A1, MEMSTR_0:47;

then A19: s = Exec (i,s) by A16, SCMPDS_2:44;

now :: thesis: for n being Nat holds CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS

then
not P +* (Macro i) halts_on s
;let n be Nat; :: thesis: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS

Comput ((P +* (Macro i)),s,n) = s by A18, A16, A17, EXTPRO_1:27, SCMPDS_2:44

.= Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by A19, A17

.= Comput ((P +* (Macro i)),s,(0 + 1)) by EXTPRO_1:3 ;

hence CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS by A13, A15; :: thesis: verum

end;Comput ((P +* (Macro i)),s,n) = s by A18, A16, A17, EXTPRO_1:27, SCMPDS_2:44

.= Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by A19, A17

.= Comput ((P +* (Macro i)),s,(0 + 1)) by EXTPRO_1:3 ;

hence CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS by A13, A15; :: thesis: verum

hence Exec (i,s) = IExec ((Load i),P,s) by A7, SCMPDS_4:def 7; :: thesis: verum

suppose A20:
IC (Comput ((P +* (Macro i)),s,1)) = 1
; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) =
(P +* (Macro i)) . 1
by A20, PBOOLE:143

.= halt SCMPDS by A3, A5, A7, GRFUNC_1:2 ;

hence Exec (i,s) = IExec ((Load i),P,s) by A2, A10, EXTPRO_1:def 9; :: thesis: verum

end;.= halt SCMPDS by A3, A5, A7, GRFUNC_1:2 ;

hence Exec (i,s) = IExec ((Load i),P,s) by A2, A10, EXTPRO_1:def 9; :: thesis: verum