thus f,a := b is parahalting :: thesis: f,a := b is keeping_0

proof

set Ma = Macro (f,a := b);
let s be State of ; :: according to AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis: ( not (Macro (f,a := b)) +* (Start-At (insloc 0 )) c= s or ProgramPart s halts_on s )
assume A43: (Macro (f,a := b)) +* (Start-At (insloc 0 )) c= s ; :: thesis: ProgramPart s halts_on s
A44: Macro (f,a := b) c= s by A43, SCMFSA6B:5;
take 1 ; :: according to AMI_1:def 20 :: thesis: ( IC (Computation s,1) in dom (ProgramPart s) & (ProgramPart s) . (IC (Computation s,1)) = halt SCM+FSA )
IC (Computation s,1) in NAT by AMI_1:def 4;
hence IC (Computation s,1) in dom (ProgramPart s) by AMI_1:143; :: thesis: (ProgramPart s) . (IC (Computation s,1)) = halt SCM+FSA
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A45: IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
Start-At (insloc 0 ) c= (Macro (f,a := b)) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then Start-At (insloc 0 ) c= s by A43, XBOOLE_1:1;
then A46: IC s = (Start-At (insloc 0 )) . (IC SCM+FSA ) by A45, GRFUNC_1:8
.= insloc 0 by FUNCOP_1:87 ;
then A47: IC (Exec (f,a := b),s) = Next (insloc 0 ) by SCMFSA_2:99
.= insloc (0 + 1) ;
insloc 1 in dom (Macro (f,a := b)) by SCMFSA6B:32;
then (Macro (f,a := b)) . (insloc 1) = s . (insloc 1) by A44, GRFUNC_1:8;
then A48: s . (insloc 1) = halt SCM+FSA by SCMFSA6B:33;
insloc 0 in dom (Macro (f,a := b)) by SCMFSA6B:32;
then A49: (Macro (f,a := b)) . (insloc 0 ) = s . (insloc 0 ) by A44, GRFUNC_1:8;
Computation s,(0 + 1) = Following (Computation s,0 ) by AMI_1:14
.= Following s by AMI_1:13
.= Exec (f,a := b),s by A46, A49, SCMFSA6B:33 ;
then CurInstr (Computation s,1) = halt SCM+FSA by A48, A47, AMI_1:def 13;
hence (ProgramPart s) . (IC (Computation s,1)) = halt SCM+FSA by AMI_1:145; :: thesis: verum

end;

thus f,a := b is keeping_0 :: thesis: verum

proof

set Ma = Macro (f,a := b);
let s be State of ; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: ( not (Macro (f,a := b)) +* (Start-At (insloc 0 )) c= s or for b₁ being Element of NAT holds (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 ) )
assume A50: (Macro (f,a := b)) +* (Start-At (insloc 0 )) c= s ; :: thesis: for b₁ being Element of NAT holds (Computation s,b₁) . (intloc 0 ) = s . (intloc 0 )
then A51: Macro (f,a := b) c= s by SCMFSA6B:5;
let k be Element of NAT ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
dom (Start-At (insloc 0 )) = {(IC SCM+FSA )} by FUNCOP_1:19;
then A52: IC SCM+FSA in dom (Start-At (insloc 0 )) by TARSKI:def 1;
Start-At (insloc 0 ) c= (Macro (f,a := b)) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then Start-At (insloc 0 ) c= s by A50, XBOOLE_1:1;
then A53: IC s = (Start-At (insloc 0 )) . (IC SCM+FSA ) by A52, GRFUNC_1:8
.= insloc 0 by FUNCOP_1:87 ;
insloc 0 in dom (Macro (f,a := b)) by SCMFSA6B:32;
then A54: (Macro (f,a := b)) . (insloc 0 ) = s . (insloc 0 ) by A51, GRFUNC_1:8;
A55: Computation s,(0 + 1) = Following (Computation s,0 ) by AMI_1:14
.= Following s by AMI_1:13
.= Exec (f,a := b),s by A53, A54, SCMFSA6B:33 ;
insloc 1 in dom (Macro (f,a := b)) by SCMFSA6B:32;
then (Macro (f,a := b)) . (insloc 1) = s . (insloc 1) by A51, GRFUNC_1:8;
then A56: s . (insloc 1) = halt SCM+FSA by SCMFSA6B:33;
IC (Exec (f,a := b),s) = Next (insloc 0 ) by A53, SCMFSA_2:99
.= insloc (0 + 1) ;
then A57: CurInstr (Computation s,1) = halt SCM+FSA by A56, A55, AMI_1:def 13;

per cases ( k = 0 or 1 <= k ) by NAT_1:14;

suppose k = 0 ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )

hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by AMI_1:13; :: thesis: verum

end;

suppose A58: 1 <= k ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )

(Computation s,1) . (intloc 0 ) = s . (intloc 0 ) by A55, SCMFSA_2:99;
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by A57, A58, AMI_1:52; :: thesis: verum

end;

end;

end;