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