set I = (0,1) --> (i,(halt S));
A1: dom ((0,1) --> (i,(halt S))) = {0,1} by FUNCT_4:65;
A6: (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
A7: n in dom ((0,1) --> (i,(halt S))) and
A8: m < n ; :: thesis: m in proj1 ((0,1) --> (i,(halt S)))
( n = 0 or n = 1 ) by A1, A7, TARSKI:def 2;
then n = 0 + 1 by A8;
then m <= 0 by A8, 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 A6; :: thesis: verum