thus (f,a) := b is parahalting :: thesis: (f,a) := b is keeping_0
proof
set Ma = Macro ((f,a) := b);
let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 11,SCMFSA6C:def 1 :: thesis: for b1 being set holds
( not Macro ((f,a) := b) c= b1 or b1 halts_on s )
A67: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Macro ((f,a) := b) c= P or P halts_on s )
assume A68: Macro ((f,a) := b) c= P ; :: thesis: P halts_on s
take 1 ; :: according to EXTPRO_1:def 8 :: thesis: ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A70: dom P = NAT by PARTFUN1:def 2;
thus IC (Comput (P,s,1)) in dom P by A70; :: thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A71: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A72: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A71, A67, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
then A73: IC (Exec (((f,a) := b),s)) = succ 0 by SCMFSA_2:73
.= 0 + 1 ;
A74: 1 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
A75: 0 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
A76: P . 0 = (Macro ((f,a) := b)) . 0 by A68, A75, GRFUNC_1:2
.= (f,a) := b by COMPOS_1:58 ;
A77: P . 1 = (Macro ((f,a) := b)) . 1 by A68, A74, GRFUNC_1:2
.= halt SCM+FSA by COMPOS_1:59 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec (((f,a) := b),s) by A72, A70, A76, PARTFUN1:def 6 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A73, A70, A77, PARTFUN1:def 6; :: thesis: verum
end;
thus (f,a) := b is keeping_0 :: thesis: verum
proof
set Ma = Macro ((f,a) := b);
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: for b1 being set holds
( not Macro ((f,a) := b) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A78: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Macro ((f,a) := b) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A79: Macro ((f,a) := b) c= P ; :: thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then A80: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A81: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A80, A78, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
then A82: (Macro ((f,a) := b)) . 0 = P . 0 by A79, GRFUNC_1:2;
A83: P /. (IC s) = P . (IC s) by PBOOLE:143;
A84: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec (((f,a) := b),s) by A81, A82, A83, COMPOS_1:58 ;
1 in dom (Macro ((f,a) := b)) by COMPOS_1:60;
then (Macro ((f,a) := b)) . 1 = P . 1 by A79, GRFUNC_1:2;
then A85: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec (((f,a) := b),s)) = succ 0 by A81, SCMFSA_2:73
.= 0 + 1 ;
then A86: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A85, A84, PBOOLE:143;
per cases ( k = 0 or 1 <= k ) by NAT_1:14;
suppose k = 0 ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by EXTPRO_1:2; :: thesis: verum
end;
suppose A87: 1 <= k ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A84, SCMFSA_2:73;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A86, A87, EXTPRO_1:5; :: thesis: verum
end;
end;
end;