let P be Instruction-Sequence of SCM; :: thesis: ( Euclid-Algorithm c= P implies S₁[P] )
assume A1: Euclid-Algorithm c= P ; :: thesis: S₁[P]
(1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) c= (0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) by FUNCT_4:25;
then A2: (1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) c= P by A1;
(2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) c= (1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by FUNCT_4:25;
then A3: (2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) c= P by A2;
(3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)) c= (2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by FUNCT_4:25;
then A4: (3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)) c= P by A3;
A5: dom (4 .--> (halt SCM)) = {4} ;
A6: not 3 in dom (4 .--> (halt SCM)) by TARSKI:def 1;
dom (3 .--> ((dl. 1) >0_goto 0)) = {3} ;
then A7: dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) = {3} \/ {4} by A5, FUNCT_4:def 1
.= {3,4} by ENUMSET1:1 ;
then A8: not 2 in dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by TARSKI:def 2;
dom (2 .--> ((dl. 0) := (dl. 2))) = {2} ;
then A9: dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) = {2} \/ {3,4} by A7, FUNCT_4:def 1
.= {2,3,4} by ENUMSET1:2 ;
then A10: not 1 in dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by ENUMSET1:def 1;
dom (1 .--> (Divide ((dl. 0),(dl. 1)))) = {1} ;
then A11: dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) = {1} \/ {2,3,4} by A9, FUNCT_4:def 1
.= {1,2,3,4} by ENUMSET1:4 ;
then A12: not 0 in dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) ;
0 in dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) by Th1, CARD_1:53, ENUMSET1:def 3;
hence P . 0 = ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) . 0 by A1, GRFUNC_1:2
.= (0 .--> ((dl. 2) := (dl. 1))) . 0 by A12, FUNCT_4:11
.= (dl. 2) := (dl. 1) by FUNCOP_1:72 ;
:: thesis: ( P . 1 = Divide ((dl. 0),(dl. 1)) & P . 2 = (dl. 0) := (dl. 2) & P . 3 = (dl. 1) >0_goto 0 & P halts_at 4 )
1 in dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) by A11, ENUMSET1:def 2;
hence P . 1 = ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) . 1 by A2, GRFUNC_1:2
.= (1 .--> (Divide ((dl. 0),(dl. 1)))) . 1 by A10, FUNCT_4:11
.= Divide ((dl. 0),(dl. 1)) by FUNCOP_1:72 ;
:: thesis: ( P . 2 = (dl. 0) := (dl. 2) & P . 3 = (dl. 1) >0_goto 0 & P halts_at 4 )
2 in dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) by A9, ENUMSET1:def 1;
hence P . 2 = ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) . 2 by A3, GRFUNC_1:2
.= (2 .--> ((dl. 0) := (dl. 2))) . 2 by A8, FUNCT_4:11
.= (dl. 0) := (dl. 2) by FUNCOP_1:72 ;
:: thesis: ( P . 3 = (dl. 1) >0_goto 0 & P halts_at 4 )
A13: 4 in dom (4 .--> (halt SCM)) by TARSKI:def 1;
3 in dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by A7, TARSKI:def 2;
hence P . 3 = ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) . 3 by A4, GRFUNC_1:2
.= (3 .--> ((dl. 1) >0_goto 0)) . 3 by A6, FUNCT_4:11
.= (dl. 1) >0_goto 0 by FUNCOP_1:72 ;
:: thesis: P halts_at 4
A14: 4 in dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) by A7, TARSKI:def 2;
thus P . 4 = ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) . 4 by A4, A14, GRFUNC_1:2
.= (4 .--> (halt SCM)) . 4 by A13, FUNCT_4:13
.= halt SCM by FUNCOP_1:72 ; :: according to COMPOS_1:def 13 :: thesis: verum