rng (4 .--> (halt SCM)) = {(halt SCM)} by FUNCOP_1:8;
then A1: halt SCM in rng (4 .--> (halt SCM)) by TARSKI:def 1;
rng (4 .--> (halt SCM)) c= rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by FUNCT_4:18;
then A2: halt SCM in rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by A1;
rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) c= rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by FUNCT_4:18;
then A3: halt SCM in rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by A2;
rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) c= rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) by FUNCT_4:18;
then A4: halt SCM in rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) by A3;
rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) 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