reconsider h = halt S as Element of the Object-Kind of S . 0 by COMPOS_1:def 8;
x: ((IC S),l) --> (l,h) = (Start-At (l,S)) +* (l .--> h) by FUNCT_4:def 4;
( (Start-At (l,S)) +* (l .--> (halt S)) is the carrier of S -defined & (Start-At (l,S)) +* (l .--> (halt S)) is the Object-Kind of S -compatible ) ;
then reconsider p = ((IC S),l) --> (l,(halt S)) as FinPartState of S by FUNCT_4:def 4;
A: ( p is autonomic & p is halting ) by Th10, Th12, x;
dom p = {(IC S),l} by FUNCT_4:65;
then X1: IC S in dom p by TARSKI:def 2;
IC S <> l by COMPOS_1:3;
then IC p = l by FUNCT_4:66;
then X: p is l -started by X1, COMPOS_1:def 16;
dom (l .--> h) = {l} by FUNCOP_1:19;
then C: dom (l .--> h) c= NAT ;
p | NAT = ((Start-At (l,S)) | NAT) +* ((l .--> h) | NAT) by x, FUNCT_4:75
.= {} +* ((l .--> h) | NAT) by COMPOS_1:47
.= (l .--> h) | NAT by FUNCT_4:21
.= l .--> h by C, RELAT_1:97 ;
then p | NAT <> {} ;
then not p is program-free by COMPOS_1:def 29;
hence ex b₁ being FinPartState of S st
( b₁ is autonomic & b₁ is halting & not b₁ is program-free & b₁ is l -started ) by A, X; :: thesis: verum