reconsider h = halt S as Element of the Object-Kind of S . 0 by COMPOS_1:def 8;
A1: ((IC ),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 ),l) --> (l,(halt S)) as FinPartState of S by FUNCT_4:def 4;
A2: ( p is autonomic & p is halting ) by Th10, Th12, A1;
dom p = {(IC ),l} by FUNCT_4:65;
then A3: IC in dom p by TARSKI:def 2;
IC p = l by FUNCT_4:66, COMPOS_1:3;
then A4: p is l -started by A3, COMPOS_1:def 16;
A5: dom (l .--> h) = {l} by FUNCOP_1:19;
p | NAT = ((Start-At (l,S)) | NAT) +* ((l .--> h) | NAT) by A1, FUNCT_4:75
.= {} +* ((l .--> h) | NAT) by COMPOS_1:47
.= (l .--> h) | NAT by FUNCT_4:21
.= l .--> h by A5, RELAT_1:97 ;
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 A2, A4; :: thesis: verum