let s be State of SCM+FSA ; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan s holds
CurInstr (Computation (s +* (loop I)),k) <> halt SCM+FSA
let I be InitHalting Program of SCM+FSA ; :: thesis: ( Initialized I c= s implies for k being Element of NAT st k <= LifeSpan s holds
CurInstr (Computation (s +* (loop I)),k) <> halt SCM+FSA )
assume A1:
Initialized I c= s
; :: thesis: for k being Element of NAT st k <= LifeSpan s holds
CurInstr (Computation (s +* (loop I)),k) <> halt SCM+FSA
then A2:
s is halting
by AMI_1:def 26;
set s2 = s +* (loop I);
hereby :: thesis: verum
let k be
Element of
NAT ;
:: thesis: ( k <= LifeSpan s implies not CurInstr (Computation (s +* (loop I)),k) = halt SCM+FSA )assume A3:
k <= LifeSpan s
;
:: thesis: not CurInstr (Computation (s +* (loop I)),k) = halt SCM+FSA set lk =
IC (Computation s,k);
A4:
IC (Computation s,k) in dom I
by A1, Def1;
A5:
IC (Computation s,k) = IC (Computation (s +* (loop I)),k)
by A1, A2, A3, Th65, AMI_1:121;
A6:
dom I = dom (loop I)
by FUNCT_4:105;
assume A7:
CurInstr (Computation (s +* (loop I)),k) = halt SCM+FSA
;
:: thesis: contradictionA8:
CurInstr (Computation (s +* (loop I)),k) =
(s +* (loop I)) . (IC (Computation s,k))
by A5, AMI_1:54
.=
(loop I) . (IC (Computation s,k))
by A4, A6, FUNCT_4:14
;
(loop I) . (IC (Computation s,k)) in rng (loop I)
by A4, A6, FUNCT_1:def 5;
hence
contradiction
by A7, A8, SCMFSA8C:107;
:: thesis: verum
end;