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 ;

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

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;

hereby :: thesis: verum

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

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

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

end;

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

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

let b be Int_position; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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;

suppose InsCode i = 0 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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

end;

suppose InsCode i = 14 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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;

suppose InsCode i = 4 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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;

suppose InsCode i = 5 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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;

suppose InsCode i = 6 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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;

end;

end;

A17: Following ((P +* (Macro i)),s) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0)))
.= 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

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;

then not P +* (Macro i) halts_on s ;
hence Exec (i,s) = IExec ((Load i),P,s) by A7, SCMPDS_4:def 7; :: thesis: verum

end;

end;

end;

end;

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;

end;