thus f :=<0,...,0> a is parahalting :: thesis: f :=<0,...,0> a is keeping_0
proof
set Ma = Macro (f :=<0,...,0> a);
let s be State of SCM+FSA ; :: according to AMI_1:def 26,SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis: ( not (Macro (f :=<0,...,0> a)) +* (Start-At 0 ,SCM+FSA ) c= s or ProgramPart s halts_on s )
assume A8: (Macro (f :=<0,...,0> a)) +* (Start-At 0 ,SCM+FSA ) c= s ; :: thesis: ProgramPart s halts_on s
A9: Macro (f :=<0,...,0> a) c= s by A8, SCMFSA6B:5;
take 1 ; :: according to AMI_1:def 20 :: 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 A10: IC SCM+FSA in dom (Start-At 0 ,SCM+FSA ) by TARSKI:def 1;
Start-At 0 ,SCM+FSA c= (Macro (f :=<0,...,0> a)) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:26;
then Start-At 0 ,SCM+FSA c= s by A8, XBOOLE_1:1;
then A11: IC s = (Start-At 0 ,SCM+FSA ) . (IC SCM+FSA ) by A10, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
then A12: IC (Exec (f :=<0,...,0> a),s) = succ 0 by SCMFSA_2:101
.= 0 + 1 ;
1 in dom (Macro (f :=<0,...,0> a)) by SCMFSA6B:32;
then (Macro (f :=<0,...,0> a)) . 1 = s . 1 by A9, GRFUNC_1:8;
then A13: s . 1 = halt SCM+FSA by SCMFSA6B:33;
0 in dom (Macro (f :=<0,...,0> a)) by SCMFSA6B:32;
then A14: (Macro (f :=<0,...,0> a)) . 0 = s . 0 by A9, 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 AMI_1:14
.= Following (ProgramPart s),s by AMI_1:13
.= Exec (f :=<0,...,0> a),s by A11, A14, Y, SCMFSA6B:33 ;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCM+FSA by A12, A13, Z, NX, AMI_1:def 13;
hence CurInstr (ProgramPart s),(Comput (ProgramPart s),s,1) = halt SCM+FSA ; :: thesis: verum
end;
thus f :=<0,...,0> a is keeping_0 :: thesis: verum
proof
set Ma = Macro (f :=<0,...,0> a);
let s be State of SCM+FSA ; :: according to SCMFSA6B:def 4,SCMFSA6C:def 2 :: thesis: ( not (Macro (f :=<0,...,0> a)) +* (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 A15: (Macro (f :=<0,...,0> a)) +* (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 A16: Macro (f :=<0,...,0> a) 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 A17: IC SCM+FSA in dom (Start-At 0 ,SCM+FSA ) by TARSKI:def 1;
Start-At 0 ,SCM+FSA c= (Macro (f :=<0,...,0> a)) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:26;
then Start-At 0 ,SCM+FSA c= s by A15, XBOOLE_1:1;
then A18: IC s = (Start-At 0 ,SCM+FSA ) . (IC SCM+FSA ) by A17, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
0 in dom (Macro (f :=<0,...,0> a)) by SCMFSA6B:32;
then A19: (Macro (f :=<0,...,0> a)) . 0 = s . 0 by A16, 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;
A20: Comput (ProgramPart s),s,(0 + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,0 ) by AMI_1:14
.= Following (ProgramPart s),s by AMI_1:13
.= Exec (f :=<0,...,0> a),s by A18, A19, Y, SCMFSA6B:33 ;
1 in dom (Macro (f :=<0,...,0> a)) by SCMFSA6B:32;
then (Macro (f :=<0,...,0> a)) . 1 = s . 1 by A16, GRFUNC_1:8;
then A21: s . 1 = halt SCM+FSA by SCMFSA6B:33;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,1) by AMI_1:123;
IC (Exec (f :=<0,...,0> a),s) = succ 0 by A18, SCMFSA_2:101
.= 0 + 1 ;
then A22: CurInstr (ProgramPart (Comput (ProgramPart s),s,1)),(Comput (ProgramPart s),s,1) = halt SCM+FSA by A21, A20, Z, AMI_1:def 13;
per cases ( k = 0 or 1 <= k ) by NAT_1:14;
end;
end;