let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being parahalting Instruction of SCM+FSA holds NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for i being parahalting Instruction of SCM+FSA holds NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))
let i be parahalting Instruction of SCM+FSA; :: thesis: NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))
set Mi = Macro i;
set sI = s +* (Initialize ((intloc 0) .--> 1));
set pI = P +* (Macro i);
A1: Macro i c= P +* (Macro i) by FUNCT_4:26;
set Is = Initialized s;
set IC1 = IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1));
reconsider Mi = Macro i as parahalting Program of SCM+FSA ;
A4: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then B4: Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1)) by A4, XBOOLE_1:1;
then A3: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) in dom Mi by SCMFSA6B:def 2, FUNCT_4:26;

A5: now

set X = (Data-Locations SCM+FSA) \/ {(IC )};
assume A6: Result ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) = Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: NPP (IExec (Mi,P,s)) = NPP (Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))))
thus NPP (IExec (Mi,P,s)) = (NPP (Result ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))))) +* (NPP (s | NAT)) by COMPOS_1:221
.= (NPP (Result ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))))) +* {}
.= NPP (Result ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))))) by FUNCT_4:22
.= NPP (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) by A6 ; :: thesis: verum

end;

A24: 1 in dom Mi by COMPOS_1:147;
A25: 0 in dom Mi by COMPOS_1:147;
A26: Mi . 0 = i by COMPOS_1:148;
XX2: Initialize ((intloc 0) .--> 1) c= Initialized Mi by FUNCT_4:26;
XX3: IC in dom (Initialize ((intloc 0) .--> 1)) by COMPOS_1:225;
then XX: IC (s +* (Initialize ((intloc 0) .--> 1))) = IC (Initialize ((intloc 0) .--> 1)) by FUNCT_4:14
.= IC (Initialized Mi) by XX2, GRFUNC_1:8, XX3
.= 0 by SCMFSA6A:25 ;
A28: Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1)) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0))) by EXTPRO_1:4
.= Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) by EXTPRO_1:3
.= Exec (((P +* (Macro i)) . (IC (s +* (Initialize ((intloc 0) .--> 1))))),(s +* (Initialize ((intloc 0) .--> 1)))) by PBOOLE:158
.= Exec (((P +* (Macro i)) . 0),(s +* (Initialize ((intloc 0) .--> 1)))) by XX
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A26, GRFUNC_1:8, A1, A25 ;

per cases ( IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 or IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 ) by A3, COMPOS_1:147;

suppose A29: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 ; :: thesis: NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))

then A30: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 0 by PBOOLE:158
.= i by A26, FUNCT_4:14, A25 ;
succ (IC (s +* (Initialize ((intloc 0) .--> 1)))) = succ 0 by XX
.= 1 ;
then A31: InsCode i in {0,6,7,8} by A28, A29, SCMFSA6A:23;

hereby :: thesis: verum

per cases ( InsCode i = 0 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A31, ENUMSET1:def 2;

suppose InsCode i = 0 ; :: thesis: NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))

then A32: i = halt SCM+FSA by SCMFSA_2:122;
then P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by A30, EXTPRO_1:30;
hence NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s)) by A5, A28, A30, A32, EXTPRO_1:def 8; :: thesis: verum

end;

suppose A33: ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; :: thesis: NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))

A34: now

let a be Int-Location ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

per cases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A33;

suppose InsCode i = 6 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Element of NAT st i = goto l by SCMFSA_2:59;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:95; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Element of NAT ex b being Int-Location st i = b =0_goto l by SCMFSA_2:60;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:96; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Element of NAT ex b being Int-Location st i = b >0_goto l by SCMFSA_2:61;
hence (s +* (Initialize ((intloc 0) .--> 1))) . a = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . a by SCMFSA_2:97; :: thesis: verum

end;

end;

end;

A36: now

let f be FinSeq-Location ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

per cases ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A33;

suppose InsCode i = 6 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Element of NAT st i = goto l by SCMFSA_2:59;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:95; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:60;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:96; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . b₁

then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:61;
hence (s +* (Initialize ((intloc 0) .--> 1))) . f = (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) . f by SCMFSA_2:97; :: thesis: verum

end;

end;

end;

A37: NPP (s +* (Initialize ((intloc 0) .--> 1))) = NPP (Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))) by A34, A36, SCMFSA_2:138, A28, A29, XX;
A38: Following ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1)))) = Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0))) by EXTPRO_1:3
.= Exec (i,(s +* (Initialize ((intloc 0) .--> 1)))) by A28, EXTPRO_1:4 ;

now

let n be Element of NAT ; :: thesis: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n))) <> halt SCM+FSA
NPP (Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n)) = NPP (s +* (Initialize ((intloc 0) .--> 1))) by A37, A38, AMISTD_2:70
.= NPP (Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0)))) by A37, A38, EXTPRO_1:3
.= NPP (Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1))) by EXTPRO_1:4 ;
then IC (Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n)) = IC (NPP (Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) by COMPOS_1:240
.= IC (Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1)) by COMPOS_1:240 ;
then CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n))) = i by A30;
hence CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n))) <> halt SCM+FSA by A33, SCMFSA_2:124; :: thesis: verum

end;

then A39: not P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:30;
Mi c= P +* Mi by FUNCT_4:26;
hence NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s)) by A39, B4, SCMFSA6B:def 3; :: thesis: verum

end;

end;

end;

end;

suppose A41: IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 ; :: thesis: NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))

A42: Mi c= Initialized Mi by SCMFSA6A:26;
(Initialized Mi) . 1 = halt SCM+FSA by SCMFSA6B:33;
then A43: Mi . 1 = halt SCM+FSA by A42, A24, GRFUNC_1:8;
A44: CurInstr ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) = (P +* Mi) . 1 by A41, PBOOLE:158
.= halt SCM+FSA by A43, GRFUNC_1:8, A1, A24 ;
then P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:30;
hence NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s)) by A5, A28, A44, EXTPRO_1:def 8; :: thesis: verum

end;

end;