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 SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis: ( not Start-At (0,SCM+FSA) c= s or for b1 being set holds
( not Macro (f :=<0,...,0> a) c= b1 or b1 halts_on s ) )
assume A12: Start-At (0,SCM+FSA) c= s ; :: thesis: for b1 being set holds
( not Macro (f :=<0,...,0> a) c= b1 or b1 halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not Macro (f :=<0,...,0> a) c= P or P halts_on s )
assume A13: Macro (f :=<0,...,0> a) c= P ; :: thesis: P halts_on s
A14: Macro (f :=<0,...,0> a) c= P by A13;
take 1 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A15: dom P = NAT by PARTFUN1:def 4;
thus IC (Comput (P,s,1)) in dom P by A15; :: thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A16: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A17: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A16, GRFUNC_1:8, A12
.= 0 by FUNCOP_1:87 ;
then A18: IC (Exec ((f :=<0,...,0> a),s)) = succ 0 by SCMFSA_2:101
.= 0 + 1 ;
A19: 1 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:147;
A20: 0 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:147;
A21: P . 0 = (Macro (f :=<0,...,0> a)) . 0 by A14, A20, GRFUNC_1:8
.= f :=<0,...,0> a by COMPOS_1:148 ;
A22: P . 1 = (Macro (f :=<0,...,0> a)) . 1 by A14, A19, GRFUNC_1:8
.= halt SCM+FSA by COMPOS_1:148 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:4
.= Following (P,s) by EXTPRO_1:3
.= Exec ((f :=<0,...,0> a),s) by A17, A15, PARTFUN1:def 8, A21 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A18, A15, PARTFUN1:def 8, A22; :: 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 Start-At (0,SCM+FSA) c= s or for b1 being set holds
( not Macro (f :=<0,...,0> a) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) ) )
assume A23: Start-At (0,SCM+FSA) c= s ; :: thesis: for b1 being set holds
( not Macro (f :=<0,...,0> a) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not Macro (f :=<0,...,0> a) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A24: Macro (f :=<0,...,0> a) 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:19;
then A25: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A26: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A25, GRFUNC_1:8, A23
.= 0 by FUNCOP_1:87 ;
0 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:147;
then A27: (Macro (f :=<0,...,0> a)) . 0 = P . 0 by A24, GRFUNC_1:8;
A28: P /. (IC s) = P . (IC s) by PBOOLE:158;
A29: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:4
.= Following (P,s) by EXTPRO_1:3
.= Exec ((f :=<0,...,0> a),s) by A26, A27, A28, COMPOS_1:148 ;
1 in dom (Macro (f :=<0,...,0> a)) by COMPOS_1:147;
then (Macro (f :=<0,...,0> a)) . 1 = P . 1 by A24, GRFUNC_1:8;
then A30: P . 1 = halt SCM+FSA by COMPOS_1:148;
IC (Exec ((f :=<0,...,0> a),s)) = succ 0 by A26, SCMFSA_2:101
.= 0 + 1 ;
then A31: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A30, A29, PBOOLE:158;
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:3; :: thesis: verum
end;
suppose A32: 1 <= k ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A29, SCMFSA_2:101;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A31, A32, EXTPRO_1:6; :: thesis: verum
end;
end;
end;