set I = (0,1) --> (i,(halt S));
A1: dom ((0,1) --> (i,(halt S))) = {0,1} by FUNCT_4:65;
A2: (0,1) --> (i,(halt S)) is initial

proof

let m, n be Nat; :: according to AFINSQ_1:def 13 :: thesis: ( not n in proj1 ((0,1) --> (i,(halt S))) or n <= m or m in proj1 ((0,1) --> (i,(halt S))) )
assume that
A3: n in dom ((0,1) --> (i,(halt S))) and
A4: m < n ; :: thesis: m in proj1 ((0,1) --> (i,(halt S)))
( n = 0 or n = 1 ) by A1, A3, TARSKI:def 2;
then n = 0 + 1 by A4;
then m <= 0 by A4, NAT_1:13;
then m = 0 ;
hence m in proj1 ((0,1) --> (i,(halt S))) by A1, TARSKI:def 2; :: thesis: verum

end;

thus (0,1) --> (i,(halt S)) is Program of S by A2; :: thesis: verum