rng (4 .--> ()) = {()} by FUNCOP_1:8;
then A1: halt SCM in rng (4 .--> ()) by TARSKI:def 1;
rng (4 .--> ()) c= rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())) by FUNCT_4:18;
then A2: halt SCM in rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())) by A1;
rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())) c= rng ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ()))) by FUNCT_4:18;
then A3: halt SCM in rng ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ()))) by A2;
rng ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ()))) c= rng ((1 .--> (Divide ((),(dl. 1)))) +* ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())))) by FUNCT_4:18;
then A4: halt SCM in rng ((1 .--> (Divide ((),(dl. 1)))) +* ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())))) by A3;
rng ((1 .--> (Divide ((),(dl. 1)))) +* ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())))) c= rng Euclid-Algorithm by FUNCT_4:18;
then halt SCM in rng Euclid-Algorithm by A4;
hence not Euclid-Algorithm is halt-free ; :: thesis: verum