let P be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( Euclide-Algorithm c= P implies S₁[P] )
assume A1: Euclide-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:26;
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, XBOOLE_1:1;
(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:26;
then A3: (2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0 )) +* (4 .--> (halt SCM ))) c= P by A2, XBOOLE_1:1;
(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:26;
then A4: (3 .--> ((dl. 1) >0_goto 0 )) +* (4 .--> (halt SCM )) c= P by A3, XBOOLE_1:1;
A5: dom (4 .--> (halt SCM )) = {4} by FUNCOP_1:19;
then A6: not 3 in dom (4 .--> (halt SCM )) by TARSKI:def 1;
dom (3 .--> ((dl. 1) >0_goto 0 )) = {3} by FUNCOP_1:19;
then A7: dom ((3 .--> ((dl. 1) >0_goto 0 )) +* (4 .--> (halt SCM ))) = {3} \/ {4} by A5, FUNCT_4:def 1
.= {3,4} by ENUMSET1:41 ;
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} by FUNCOP_1:19;
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:42 ;
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} by FUNCOP_1:19;
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:44 ;
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 Th4, CARD_1:91, 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:8
.= (0 .--> ((dl. 2) := (dl. 1))) . 0 by A12, FUNCT_4:12
.= (dl. 2) := (dl. 1) by FUNCOP_1:87 ;
:: 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:8
.= (1 .--> (Divide (dl. 0 ),(dl. 1))) . 1 by A10, FUNCT_4:12
.= Divide (dl. 0 ),(dl. 1) by FUNCOP_1:87 ;
:: 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:8
.= (2 .--> ((dl. 0 ) := (dl. 2))) . 2 by A8, FUNCT_4:12
.= (dl. 0 ) := (dl. 2) by FUNCOP_1:87 ;
:: thesis: ( P . 3 = (dl. 1) >0_goto 0 & P halts_at 4 )
A13: 4 in dom (4 .--> (halt SCM )) by A5, 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:8
.= (3 .--> ((dl. 1) >0_goto 0 )) . 3 by A6, FUNCT_4:12
.= (dl. 1) >0_goto 0 by FUNCOP_1:87 ;
:: thesis: P halts_at 4
X: 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, X, GRFUNC_1:8
.= (4 .--> (halt SCM )) . 4 by A13, FUNCT_4:14
.= halt SCM by FUNCOP_1:87 ; :: according to COMPOS_1:def 21 :: thesis: verum