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 SCM+FSA; :: according to EXTPRO_1:def 10,SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis: ( not (Macro ((f,a) := b)) +* (Start-At (0,SCM+FSA)) c= s or ProgramPart s halts_on s )
assume A43: (Macro ((f,a) := b)) +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: ProgramPart s halts_on s
A44: Macro ((f,a) := b) c= s by A43, SCMFSA6B:5;
take 1 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,1)) in proj1 (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCM+FSA )
IC (Comput ((ProgramPart s),s,1)) in NAT ;
hence IC (Comput ((ProgramPart s),s,1)) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;
then A45: IC SCM+FSA in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
Start-At (0,SCM+FSA) c= (Macro ((f,a) := b)) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= s by A43, XBOOLE_1:1;
then A46: IC s = (Start-At (0,SCM+FSA)) . (IC SCM+FSA) by A45, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
then A47: IC (Exec (((f,a) := b),s)) = succ 0 by SCMFSA_2:99
.= 0 + 1 ;
1 in dom (Macro ((f,a) := b)) by SCMFSA6B:32;
then (Macro ((f,a) := b)) . 1 = s . 1 by A44, GRFUNC_1:8;
then A48: s . 1 = halt SCM+FSA by COMPOS_1:148, SCMFSA6B:33;
0 in dom (Macro ((f,a) := b)) by SCMFSA6B:32;
then A49: (Macro ((f,a) := b)) . 0 = s . 0 by A44, GRFUNC_1:8;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s),s,1))) /. (IC (Comput ((ProgramPart s),s,1))) = (Comput ((ProgramPart s),s,1)) . (IC (Comput ((ProgramPart s),s,1))) by COMPOS_1:38;
NX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,1)) by AMI_1:123;
Comput ((ProgramPart s),s,(0 + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,0))) by EXTPRO_1:4
.= Following ((ProgramPart s),s) by EXTPRO_1:3
.= Exec (((f,a) := b),s) by A46, A49, Y, COMPOS_1:148, SCMFSA6B:33 ;
then CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCM+FSA by A48, A47, Z, NX, AMI_1:def 13;
hence CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,1))) = halt SCM+FSA ; :: thesis: verum
end;
thus (f,a) := b is keeping_0 :: thesis: verum
proof
set Ma = Macro ((f,a) := b);
let s be State of SCM+FSA; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: ( not (Macro ((f,a) := b)) +* (Start-At (0,SCM+FSA)) c= s or for b1 being Element of NAT holds (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0) )
assume A50: (Macro ((f,a) := b)) +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: for b1 being Element of NAT holds (Comput ((ProgramPart s),s,b1)) . (intloc 0) = s . (intloc 0)
then A51: Macro ((f,a) := b) c= s by SCMFSA6B:5;
let k be Element of NAT ; :: thesis: (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;
then A52: IC SCM+FSA in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
Start-At (0,SCM+FSA) c= (Macro ((f,a) := b)) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= s by A50, XBOOLE_1:1;
then A53: IC s = (Start-At (0,SCM+FSA)) . (IC SCM+FSA) by A52, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
0 in dom (Macro ((f,a) := b)) by SCMFSA6B:32;
then A54: (Macro ((f,a) := b)) . 0 = s . 0 by A51, GRFUNC_1:8;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s),s,1))) /. (IC (Comput ((ProgramPart s),s,1))) = (Comput ((ProgramPart s),s,1)) . (IC (Comput ((ProgramPart s),s,1))) by COMPOS_1:38;
A55: Comput ((ProgramPart s),s,(0 + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,0))) by EXTPRO_1:4
.= Following ((ProgramPart s),s) by EXTPRO_1:3
.= Exec (((f,a) := b),s) by A53, A54, Y, COMPOS_1:148, SCMFSA6B:33 ;
1 in dom (Macro ((f,a) := b)) by SCMFSA6B:32;
then (Macro ((f,a) := b)) . 1 = s . 1 by A51, GRFUNC_1:8;
then A56: s . 1 = halt SCM+FSA by COMPOS_1:148, SCMFSA6B:33;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,1)) by AMI_1:123;
IC (Exec (((f,a) := b),s)) = succ 0 by A53, SCMFSA_2:99
.= 0 + 1 ;
then A57: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,1))),(Comput ((ProgramPart s),s,1))) = halt SCM+FSA by A56, A55, Z, AMI_1:def 13;
per cases ( k = 0 or 1 <= k ) by NAT_1:14;
end;
end;