:: AMI_4 semantic presentation begin set a = dl. 0; set b = dl. 1; set c = dl. 2; Lm1: ( dl. 0 <> dl. 1 & dl. 1 <> dl. 2 ) by AMI_3:10; Lm2: dl. 2 <> dl. 0 by AMI_3:10; begin definition func Euclide-Algorithm -> NAT -defined the InstructionsF of SCM -valued finite Function equals :: AMI_4:def 1 (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))))); coherence (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))))) is NAT -defined the InstructionsF of SCM -valued finite Function ; end; :: deftheorem defines Euclide-Algorithm AMI_4:def_1_:_ Euclide-Algorithm = (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))))); defpred S1[ Instruction-Sequence of SCM] means ( \$1 . 0 = (dl. 2) := (dl. 1) & \$1 . 1 = Divide ((dl. 0),(dl. 1)) & \$1 . 2 = (dl. 0) := (dl. 2) & \$1 . 3 = (dl. 1) >0_goto 0 & \$1 halts_at 4 ); set IN0 = 0 .--> ((dl. 2) := (dl. 1)); set IN1 = 1 .--> (Divide ((dl. 0),(dl. 1))); set IN2 = 2 .--> ((dl. 0) := (dl. 2)); set IN3 = 3 .--> ((dl. 1) >0_goto 0); set IN4 = 4 .--> (halt SCM); set EA3 = (3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)); set EA2 = (2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))); set EA1 = (1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))); set EA0 = (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))))); theorem Th1: :: AMI_4:1 dom Euclide-Algorithm = 5 proof ( dom (3 .--> ((dl. 1) >0_goto 0)) = {3} & dom (4 .--> (halt SCM)) = {4} ) by FUNCOP_1:13; then A1: dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) = {3} \/ {4} by FUNCT_4:def_1 .= {3,4} by ENUMSET1:1 ; A2: dom (1 .--> (Divide ((dl. 0),(dl. 1)))) = {1} by FUNCOP_1:13; dom (2 .--> ((dl. 0) := (dl. 2))) = {2} by FUNCOP_1:13; then dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) = {2} \/ {3,4} by A1, FUNCT_4:def_1 .= {2,3,4} by ENUMSET1:2 ; then A3: 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 A2, FUNCT_4:def_1 .= {1,2,3,4} by ENUMSET1:4 ; dom (0 .--> ((dl. 2) := (dl. 1))) = {0} by FUNCOP_1:13; then 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)))))) = {0} \/ {1,2,3,4} by A3, FUNCT_4:def_1 .= 5 by CARD_1:53, ENUMSET1:7 ; hence dom Euclide-Algorithm = 5 ; ::_thesis: verum end; Lm3: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds S1[P] proof let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies S1[P] ) assume A1: Euclide-Algorithm c= P ; ::_thesis: S1[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, 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:25; 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:25; 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:13; then A6: not 3 in dom (4 .--> (halt SCM)) by TARSKI:def_1; dom (3 .--> ((dl. 1) >0_goto 0)) = {3} by FUNCOP_1:13; 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} by FUNCOP_1:13; 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} by FUNCOP_1:13; 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 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: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 end; begin theorem Th2: :: AMI_4:2 for s being State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 0 holds ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) proof let s be State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 0 holds ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for k being Element of NAT st IC (Comput (P,s,k)) = 0 holds ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for k being Element of NAT st IC (Comput (P,s,k)) = 0 holds ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) let k be Element of NAT ; ::_thesis: ( IC (Comput (P,s,k)) = 0 implies ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) ) assume A2: IC (Comput (P,s,k)) = 0 ; ::_thesis: ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) A3: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by EXTPRO_1:6 .= Exec (((dl. 2) := (dl. 1)),(Comput (P,s,k))) by A1, A2, Lm3 ; hence IC (Comput (P,s,(k + 1))) = succ (IC (Comput (P,s,k))) by AMI_3:2 .= 1 by A2 ; ::_thesis: ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) ) thus ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) by A3, AMI_3:2, AMI_3:10; ::_thesis: (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) thus (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) by A3, AMI_3:2; ::_thesis: verum end; theorem Th3: :: AMI_4:3 for s being State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 1 holds ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) proof let s be State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 1 holds ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for k being Element of NAT st IC (Comput (P,s,k)) = 1 holds ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for k being Element of NAT st IC (Comput (P,s,k)) = 1 holds ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) let k be Element of NAT ; ::_thesis: ( IC (Comput (P,s,k)) = 1 implies ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) ) assume A2: IC (Comput (P,s,k)) = 1 ; ::_thesis: ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) A3: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by EXTPRO_1:6 .= Exec ((Divide ((dl. 0),(dl. 1))),(Comput (P,s,k))) by A1, A2, Lm3 ; hence IC (Comput (P,s,(k + 1))) = succ (IC (Comput (P,s,k))) by AMI_3:6 .= 2 by A2 ; ::_thesis: ( (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) thus ( (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) by A3, Lm1, Lm2, AMI_3:6; ::_thesis: verum end; theorem Th4: :: AMI_4:4 for s being State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 2 holds ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) proof let s be State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 2 holds ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for k being Element of NAT st IC (Comput (P,s,k)) = 2 holds ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for k being Element of NAT st IC (Comput (P,s,k)) = 2 holds ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) let k be Element of NAT ; ::_thesis: ( IC (Comput (P,s,k)) = 2 implies ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) ) assume A2: IC (Comput (P,s,k)) = 2 ; ::_thesis: ( IC (Comput (P,s,(k + 1))) = 3 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) A3: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by EXTPRO_1:6 .= Exec (((dl. 0) := (dl. 2)),(Comput (P,s,k))) by A1, A2, Lm3 ; hence IC (Comput (P,s,(k + 1))) = succ (IC (Comput (P,s,k))) by AMI_3:2 .= 3 by A2 ; ::_thesis: ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) thus (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 2) by A3, AMI_3:2; ::_thesis: ( (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) thus ( (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) by A3, AMI_3:2, AMI_3:10; ::_thesis: verum end; theorem Th5: :: AMI_4:5 for s being State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 3 holds ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) proof let s be State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k being Element of NAT st IC (Comput (P,s,k)) = 3 holds ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for k being Element of NAT st IC (Comput (P,s,k)) = 3 holds ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for k being Element of NAT st IC (Comput (P,s,k)) = 3 holds ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) let k be Element of NAT ; ::_thesis: ( IC (Comput (P,s,k)) = 3 implies ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) ) assume A2: IC (Comput (P,s,k)) = 3 ; ::_thesis: ( ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) & ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) A3: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by EXTPRO_1:6 .= Exec (((dl. 1) >0_goto 0),(Comput (P,s,k))) by A1, A2, Lm3 ; hence ( (Comput (P,s,k)) . (dl. 1) > 0 implies IC (Comput (P,s,(k + 1))) = 0 ) by AMI_3:9; ::_thesis: ( ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) thus ( (Comput (P,s,k)) . (dl. 1) <= 0 implies IC (Comput (P,s,(k + 1))) = 4 ) ::_thesis: ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) proof assume (Comput (P,s,k)) . (dl. 1) <= 0 ; ::_thesis: IC (Comput (P,s,(k + 1))) = 4 hence IC (Comput (P,s,(k + 1))) = succ (IC (Comput (P,s,k))) by A3, AMI_3:9 .= 4 by A2 ; ::_thesis: verum end; thus ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) by A3, AMI_3:9; ::_thesis: verum end; theorem Th6: :: AMI_4:6 for s being State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k, i being Element of NAT st IC (Comput (P,s,k)) = 4 holds Comput (P,s,(k + i)) = Comput (P,s,k) proof let s be State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for k, i being Element of NAT st IC (Comput (P,s,k)) = 4 holds Comput (P,s,(k + i)) = Comput (P,s,k) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for k, i being Element of NAT st IC (Comput (P,s,k)) = 4 holds Comput (P,s,(k + i)) = Comput (P,s,k) ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for k, i being Element of NAT st IC (Comput (P,s,k)) = 4 holds Comput (P,s,(k + i)) = Comput (P,s,k) let k, i be Element of NAT ; ::_thesis: ( IC (Comput (P,s,k)) = 4 implies Comput (P,s,(k + i)) = Comput (P,s,k) ) assume IC (Comput (P,s,k)) = 4 ; ::_thesis: Comput (P,s,(k + i)) = Comput (P,s,k) then P halts_at IC (Comput (P,s,k)) by A1, Lm3; hence Comput (P,s,(k + i)) = Comput (P,s,k) by EXTPRO_1:20, NAT_1:11; ::_thesis: verum end; Lm4: for k being Element of NAT for s being 0 -started State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 holds ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ) proof let k be Element of NAT ; ::_thesis: for s being 0 -started State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 holds ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ) let s be 0 -started State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 holds ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 implies ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ) ) assume that A1: Euclide-Algorithm c= P and A2: ( s . (dl. 0) > 0 & s . (dl. 1) > 0 ) ; ::_thesis: ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ) A3: IC s = 0 by MEMSTR_0:def_12; defpred S2[ Element of NAT ] means ( (Comput (P,s,(4 * \$1))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * \$1))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * \$1))) = 0 ) or ( (Comput (P,s,(4 * \$1))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * \$1))) = 4 ) ) ); A4: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) set c4 = Comput (P,s,(4 * k)); set c5 = Comput (P,s,((4 * k) + 1)); set c6 = Comput (P,s,((4 * k) + 2)); set c7 = Comput (P,s,((4 * k) + 3)); set c8 = Comput (P,s,((4 * k) + 4)); A5: Comput (P,s,((4 * k) + 3)) = Comput (P,s,(((4 * k) + 2) + 1)) ; A6: Comput (P,s,((4 * k) + 4)) = Comput (P,s,(((4 * k) + 3) + 1)) ; assume A7: (Comput (P,s,(4 * k))) . (dl. 0) > 0 ; ::_thesis: ( ( not ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) & not ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) or S2[k + 1] ) assume A8: ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ; ::_thesis: S2[k + 1] A9: Comput (P,s,((4 * k) + 2)) = Comput (P,s,(((4 * k) + 1) + 1)) ; now__::_thesis:_(_(_(Comput_(P,s,(4_*_k)))_._(dl._1)_>_0_&_(Comput_(P,s,((4_*_k)_+_4)))_._(dl._0)_>_0_&_(_(_(Comput_(P,s,((4_*_k)_+_4)))_._(dl._1)_>_0_&_IC_(Comput_(P,s,((4_*_k)_+_4)))_=_0_)_or_(_(Comput_(P,s,((4_*_k)_+_4)))_._(dl._1)_=_0_&_IC_(Comput_(P,s,((4_*_k)_+_4)))_=_4_)_)_)_or_(_(Comput_(P,s,(4_*_k)))_._(dl._1)_=_0_&_(Comput_(P,s,((4_*_k)_+_4)))_._(dl._0)_>_0_&_(Comput_(P,s,((4_*_k)_+_4)))_._(dl._1)_=_0_&_IC_(Comput_(P,s,((4_*_k)_+_4)))_=_4_)_) percases ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 or (Comput (P,s,(4 * k))) . (dl. 1) = 0 ) by A8; caseA10: (Comput (P,s,(4 * k))) . (dl. 1) > 0 ; ::_thesis: ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & ( ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) > 0 & IC (Comput (P,s,((4 * k) + 4))) = 0 ) or ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) ) ) then A11: IC (Comput (P,s,((4 * k) + 1))) = 1 by A1, A8, Th2; then A12: IC (Comput (P,s,((4 * k) + 2))) = 2 by A1, A9, Th3; then A13: IC (Comput (P,s,((4 * k) + 3))) = 3 by A1, A5, Th4; then A14: (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (Comput (P,s,((4 * k) + 3))) . (dl. 1) by A1, A6, Th5; A15: ( (Comput (P,s,((4 * k) + 3))) . (dl. 0) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (Comput (P,s,((4 * k) + 2))) . (dl. 1) ) by A1, A5, A12, Th4; A16: ( (Comput (P,s,((4 * k) + 2))) . (dl. 1) = ((Comput (P,s,((4 * k) + 1))) . (dl. 0)) mod ((Comput (P,s,((4 * k) + 1))) . (dl. 1)) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (Comput (P,s,((4 * k) + 1))) . (dl. 2) ) by A1, A9, A11, Th3; A17: ( (Comput (P,s,((4 * k) + 1))) . (dl. 1) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (Comput (P,s,(4 * k))) . (dl. 1) ) by A1, A8, A10, Th2; ( (Comput (P,s,((4 * k) + 3))) . (dl. 1) > 0 implies IC (Comput (P,s,((4 * k) + 4))) = 0 ) by A1, A6, A13, Th5; hence ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & ( ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) > 0 & IC (Comput (P,s,((4 * k) + 4))) = 0 ) or ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) ) ) by A1, A6, A10, A17, A16, A13, A15, A14, Th5, NEWTON:64; ::_thesis: verum end; case (Comput (P,s,(4 * k))) . (dl. 1) = 0 ; ::_thesis: ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) hence ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) by A1, A7, A8, Th6; ::_thesis: verum end; end; end; hence S2[k + 1] ; ::_thesis: verum end; A18: S2[ 0 ] by A3, A2, EXTPRO_1:2; for k being Element of NAT holds S2[k] from NAT_1:sch_1(A18, A4); hence ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) ) ; ::_thesis: verum end; Lm5: for k being Element of NAT for s being 0 -started State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 holds ( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) ) proof let k be Element of NAT ; ::_thesis: for s being 0 -started State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 holds ( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) ) let s be 0 -started State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 holds ( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 implies ( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) ) ) assume that A1: Euclide-Algorithm c= P and A2: ( s . (dl. 0) > 0 & s . (dl. 1) > 0 ) and A3: (Comput (P,s,(4 * k))) . (dl. 1) > 0 ; ::_thesis: ( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) ) set c4 = Comput (P,s,(4 * k)); set c5 = Comput (P,s,((4 * k) + 1)); set c6 = Comput (P,s,((4 * k) + 2)); set c7 = Comput (P,s,((4 * k) + 3)); A4: ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) by A1, A2, Lm4; then A5: ( Comput (P,s,((4 * k) + 2)) = Comput (P,s,(((4 * k) + 1) + 1)) & IC (Comput (P,s,((4 * k) + 1))) = 1 ) by A1, A3, Th2; then A6: (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (Comput (P,s,((4 * k) + 1))) . (dl. 2) by A1, Th3; A7: ( Comput (P,s,((4 * k) + 3)) = Comput (P,s,(((4 * k) + 2) + 1)) & IC (Comput (P,s,((4 * k) + 2))) = 2 ) by A1, A5, Th3; then A8: ( Comput (P,s,((4 * k) + 4)) = Comput (P,s,(((4 * k) + 3) + 1)) & IC (Comput (P,s,((4 * k) + 3))) = 3 ) by A1, Th4; A9: (Comput (P,s,((4 * k) + 3))) . (dl. 0) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) by A1, A7, Th4; (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (Comput (P,s,(4 * k))) . (dl. 1) by A1, A3, A4, Th2; hence (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) by A1, A6, A8, A9, Th5; ::_thesis: (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) A10: (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (Comput (P,s,((4 * k) + 2))) . (dl. 1) by A1, A7, Th4; A11: (Comput (P,s,((4 * k) + 2))) . (dl. 1) = ((Comput (P,s,((4 * k) + 1))) . (dl. 0)) mod ((Comput (P,s,((4 * k) + 1))) . (dl. 1)) by A1, A5, Th3; ( (Comput (P,s,((4 * k) + 1))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 0) & (Comput (P,s,((4 * k) + 1))) . (dl. 1) = (Comput (P,s,(4 * k))) . (dl. 1) ) by A1, A3, A4, Th2; hence (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) by A1, A11, A8, A10, Th5; ::_thesis: verum end; Lm6: for s being 0 -started State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) ) proof let s be 0 -started State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) ) let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) ) ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) ) deffunc H1( Element of NAT ) -> Element of NAT = abs ((Comput (P,s,(4 * \$1))) . (dl. 1)); deffunc H2( Element of NAT ) -> Element of NAT = abs ((Comput (P,s,(4 * \$1))) . (dl. 0)); let x, y be Integer; ::_thesis: ( s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 implies ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) ) ) assume that A2: s . (dl. 0) = x and A3: s . (dl. 1) = y and A4: x > y and A5: y > 0 ; ::_thesis: ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) ) A6: now__::_thesis:_for_k_being_Element_of_NAT_st_H1(k)_>_0_holds_ (_H2(k_+_1)_=_H1(k)_&_H1(k_+_1)_=_H2(k)_mod_H1(k)_) let k be Element of NAT ; ::_thesis: ( H1(k) > 0 implies ( H2(k + 1) = H1(k) & H1(k + 1) = H2(k) mod H1(k) ) ) A7: ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 or (Comput (P,s,(4 * k))) . (dl. 1) = 0 ) by A1, A2, A3, A4, A5, Lm4; assume A8: H1(k) > 0 ; ::_thesis: ( H2(k + 1) = H1(k) & H1(k + 1) = H2(k) mod H1(k) ) hence H2(k + 1) = H1(k) by A1, A2, A3, A4, A5, A7, Lm5, ABSVALUE:2; ::_thesis: H1(k + 1) = H2(k) mod H1(k) A9: (Comput (P,s,(4 * k))) . (dl. 0) >= 0 by A1, A2, A3, A4, A5, Lm4; (Comput (P,s,(4 * (k + 1)))) . (dl. 1) >= 0 by A1, A2, A3, A4, A5, Lm4; hence H1(k + 1) = (Comput (P,s,(4 * (k + 1)))) . (dl. 1) by ABSVALUE:def_1 .= ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) by A1, A2, A3, A4, A5, A7, A8, Lm5, ABSVALUE:2 .= H2(k) mod H1(k) by A7, A9, INT_2:32 ; ::_thesis: verum end; reconsider x9 = x, y9 = y as Element of NAT by A4, A5, INT_1:3; A10: y9 < x9 by A4; A11: H2( 0 ) = abs x by A2, EXTPRO_1:2 .= x9 by ABSVALUE:def_1 ; A12: H1( 0 ) = abs y by A3, EXTPRO_1:2 .= y9 by ABSVALUE:def_1 ; A13: 0 < y9 by A5; consider k being Element of NAT such that A14: H2(k) = x9 gcd y9 and A15: H1(k) = 0 from NEWTON:sch_1(A13, A10, A11, A12, A6); A16: (Comput (P,s,(4 * k))) . (dl. 0) > 0 by A1, A2, A3, A4, A5, Lm4; (Comput (P,s,(4 * k))) . (dl. 1) = 0 by A15, ABSVALUE:2; then A17: IC (Comput (P,s,(4 * k))) = 4 by A1, A2, A3, A4, A5, Lm4; A18: P halts_at 4 by A1, Lm3; hence (Result (P,s)) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 0) by A17, EXTPRO_1:18 .= x gcd y by A14, A16, ABSVALUE:def_1 ; ::_thesis: ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) thus ex k being Element of NAT st P halts_at IC (Comput (P,s,k)) by A17, A18; ::_thesis: verum end; theorem Th7: :: AMI_4:7 for s being 0 -started State of SCM for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 holds (Result (P,s)) . (dl. 0) = x gcd y proof let s be 0 -started State of SCM; ::_thesis: for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 holds (Result (P,s)) . (dl. 0) = x gcd y let P be Instruction-Sequence of SCM; ::_thesis: ( Euclide-Algorithm c= P implies for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 holds (Result (P,s)) . (dl. 0) = x gcd y ) assume A1: Euclide-Algorithm c= P ; ::_thesis: for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 holds (Result (P,s)) . (dl. 0) = x gcd y let x, y be Integer; ::_thesis: ( s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 implies (Result (P,s)) . (dl. 0) = x gcd y ) assume that A2: ( s . (dl. 0) = x & s . (dl. 1) = y ) and A3: x > 0 and A4: y > 0 ; ::_thesis: (Result (P,s)) . (dl. 0) = x gcd y A5: abs y = y by A4, ABSVALUE:def_1; now__::_thesis:_(_(_x_>_y_&_(Result_(P,s))_._(dl._0)_=_x_gcd_y_)_or_(_x_=_y_&_ex_s9_being_set_st_(Result_(P,s))_._(dl._0)_=_x_gcd_y_)_or_(_y_>_x_&_ex_s9_being_set_st_(Result_(P,s))_._(dl._0)_=_x_gcd_y_)_) percases ( x > y or x = y or y > x ) by XXREAL_0:1; case x > y ; ::_thesis: (Result (P,s)) . (dl. 0) = x gcd y hence (Result (P,s)) . (dl. 0) = x gcd y by A1, A2, A4, Lm6; ::_thesis: verum end; caseA6: x = y ; ::_thesis: ex s9 being set st (Result (P,s)) . (dl. 0) = x gcd y reconsider x9 = x, y9 = y as Element of NAT by A3, A4, INT_1:3; take s9 = Comput (P,s,4); ::_thesis: (Result (P,s)) . (dl. 0) = x gcd y A7: s = Comput (P,s,(4 * 0)) by EXTPRO_1:2; A8: s9 = Comput (P,s,(4 * (0 + 1))) ; x mod y = x9 mod y9 .= 0 by A6, NAT_D:25 ; then s9 . (dl. 1) = 0 by A1, A2, A3, A4, A7, A8, Lm5; then IC s9 = 4 by A1, A2, A3, A4, A8, Lm4; then P halts_at IC s9 by A1, Lm3; hence (Result (P,s)) . (dl. 0) = s9 . (dl. 0) by EXTPRO_1:18 .= y by A1, A2, A3, A4, A7, A8, Lm5 .= x gcd y by A5, A6, NAT_D:32 ; ::_thesis: verum end; caseA9: y > x ; ::_thesis: ex s9 being set st (Result (P,s)) . (dl. 0) = x gcd y reconsider x9 = x, y9 = y as Element of NAT by A3, A4, INT_1:3; take s9 = Comput (P,s,4); ::_thesis: (Result (P,s)) . (dl. 0) = x gcd y A10: s9 = Comput (P,s,(4 * (0 + 1))) ; A11: s = Comput (P,s,(4 * 0)) by EXTPRO_1:2; then A12: s9 . (dl. 0) = y by A1, A2, A3, A4, A10, Lm5; x mod y = x9 mod y9 .= x9 by A9, NAT_D:24 ; then A13: s9 . (dl. 1) = x by A1, A2, A3, A4, A11, A10, Lm5; then IC s9 = 0 by A1, A2, A3, A4, A10, Lm4; then A14: s9 is 0 -started by MEMSTR_0:def_12; then consider k0 being Element of NAT such that A15: P halts_at IC (Comput (P,s9,k0)) by A3, A9, A12, A13, A1, Lm6; A16: P halts_at IC (Comput (P,s,(k0 + 4))) by A15, EXTPRO_1:4; (Result (P,s9)) . (dl. 0) = x gcd y by A3, A9, A12, A13, A14, A1, Lm6; hence (Result (P,s)) . (dl. 0) = x gcd y by A16, EXTPRO_1:21; ::_thesis: verum end; end; end; hence (Result (P,s)) . (dl. 0) = x gcd y ; ::_thesis: verum end; definition func Euclide-Function -> PartFunc of (FinPartSt SCM),(FinPartSt SCM) means :Def2: :: AMI_4:def 2 for p, q being FinPartState of SCM holds ( [p,q] in it iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ); existence ex b1 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st for p, q being FinPartState of SCM holds ( [p,q] in b1 iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) proof defpred S2[ set , set ] means ex x, y being Integer st ( x > 0 & y > 0 & \$1 = ((dl. 0),(dl. 1)) --> (x,y) & \$2 = (dl. 0) .--> (x gcd y) ); A1: for p, q1, q2 being set st S2[p,q1] & S2[p,q2] holds q1 = q2 proof let p, q1, q2 be set ; ::_thesis: ( S2[p,q1] & S2[p,q2] implies q1 = q2 ) given x1, y1 being Integer such that x1 > 0 and y1 > 0 and A2: p = ((dl. 0),(dl. 1)) --> (x1,y1) and A3: q1 = (dl. 0) .--> (x1 gcd y1) ; ::_thesis: ( not S2[p,q2] or q1 = q2 ) given x2, y2 being Integer such that x2 > 0 and y2 > 0 and A4: p = ((dl. 0),(dl. 1)) --> (x2,y2) and A5: q2 = (dl. 0) .--> (x2 gcd y2) ; ::_thesis: q1 = q2 A6: y1 = (((dl. 0),(dl. 1)) --> (x1,y1)) . (dl. 1) by FUNCT_4:63 .= y2 by A2, A4, FUNCT_4:63 ; x1 = (((dl. 0),(dl. 1)) --> (x1,y1)) . (dl. 0) by AMI_3:10, FUNCT_4:63 .= x2 by A2, A4, AMI_3:10, FUNCT_4:63 ; hence q1 = q2 by A3, A5, A6; ::_thesis: verum end; consider f being Function such that A7: for p, q being set holds ( [p,q] in f iff ( p in FinPartSt SCM & S2[p,q] ) ) from FUNCT_1:sch_1(A1); A8: rng f c= FinPartSt SCM proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng f or q in FinPartSt SCM ) assume q in rng f ; ::_thesis: q in FinPartSt SCM then consider p being set such that A9: [p,q] in f by XTUPLE_0:def_13; ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) by A7, A9; hence q in FinPartSt SCM by MEMSTR_0:75; ::_thesis: verum end; dom f c= FinPartSt SCM proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom f or e in FinPartSt SCM ) assume e in dom f ; ::_thesis: e in FinPartSt SCM then [e,(f . e)] in f by FUNCT_1:1; hence e in FinPartSt SCM by A7; ::_thesis: verum end; then reconsider f = f as PartFunc of (FinPartSt SCM),(FinPartSt SCM) by A8, RELSET_1:4; take f ; ::_thesis: for p, q being FinPartState of SCM holds ( [p,q] in f iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) let p, q be FinPartState of SCM; ::_thesis: ( [p,q] in f iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) thus ( [p,q] in f implies ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) by A7; ::_thesis: ( ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) implies [p,q] in f ) given x, y being Integer such that A10: ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ; ::_thesis: [p,q] in f p in FinPartSt SCM by MEMSTR_0:75; hence [p,q] in f by A7, A10; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st ( for p, q being FinPartState of SCM holds ( [p,q] in b1 iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) & ( for p, q being FinPartState of SCM holds ( [p,q] in b2 iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) holds b1 = b2 proof defpred S2[ set , set ] means ex x, y being Integer st ( x > 0 & y > 0 & \$1 = ((dl. 0),(dl. 1)) --> (x,y) & \$2 = (dl. 0) .--> (x gcd y) ); let IT1, IT2 be PartFunc of (FinPartSt SCM),(FinPartSt SCM); ::_thesis: ( ( for p, q being FinPartState of SCM holds ( [p,q] in IT1 iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) & ( for p, q being FinPartState of SCM holds ( [p,q] in IT2 iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) implies IT1 = IT2 ) assume that A11: for p, q being FinPartState of SCM holds ( [p,q] in IT1 iff S2[p,q] ) and A12: for p, q being FinPartState of SCM holds ( [p,q] in IT2 iff S2[p,q] ) ; ::_thesis: IT1 = IT2 A13: for p, q being Element of FinPartSt SCM holds ( [p,q] in IT2 iff S2[p,q] ) proof let p, q be Element of FinPartSt SCM; ::_thesis: ( [p,q] in IT2 iff S2[p,q] ) thus ( [p,q] in IT2 implies S2[p,q] ) ::_thesis: ( S2[p,q] implies [p,q] in IT2 ) proof assume A14: [p,q] in IT2 ; ::_thesis: S2[p,q] reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76; S2[p,q] by A12, A14; hence S2[p,q] ; ::_thesis: verum end; thus ( S2[p,q] implies [p,q] in IT2 ) by A12; ::_thesis: verum end; A15: for p, q being Element of FinPartSt SCM holds ( [p,q] in IT1 iff S2[p,q] ) proof let p, q be Element of FinPartSt SCM; ::_thesis: ( [p,q] in IT1 iff S2[p,q] ) thus ( [p,q] in IT1 implies S2[p,q] ) ::_thesis: ( S2[p,q] implies [p,q] in IT1 ) proof assume A16: [p,q] in IT1 ; ::_thesis: S2[p,q] reconsider p = p, q = q as FinPartState of SCM by MEMSTR_0:76; S2[p,q] by A11, A16; hence S2[p,q] ; ::_thesis: verum end; thus ( S2[p,q] implies [p,q] in IT1 ) by A11; ::_thesis: verum end; thus IT1 = IT2 from RELSET_1:sch_4(A15, A13); ::_thesis: verum end; end; :: deftheorem Def2 defines Euclide-Function AMI_4:def_2_:_ for b1 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds ( b1 = Euclide-Function iff for p, q being FinPartState of SCM holds ( [p,q] in b1 iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ); theorem Th8: :: AMI_4:8 for p being set holds ( p in dom Euclide-Function iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) ) proof let p be set ; ::_thesis: ( p in dom Euclide-Function iff ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) ) A1: dom Euclide-Function c= FinPartSt SCM by RELAT_1:def_18; A2: ( p in dom Euclide-Function iff [p,(Euclide-Function . p)] in Euclide-Function ) by FUNCT_1:1; hereby ::_thesis: ( ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) implies p in dom Euclide-Function ) assume A3: p in dom Euclide-Function ; ::_thesis: ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) then Euclide-Function . p in FinPartSt SCM by PARTFUN1:4; then A4: Euclide-Function . p is FinPartState of SCM by MEMSTR_0:76; p is FinPartState of SCM by A1, A3, MEMSTR_0:76; then ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & Euclide-Function . p = (dl. 0) .--> (x gcd y) ) by A2, A3, A4, Def2; hence ex x, y being Integer st ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) ; ::_thesis: verum end; given x, y being Integer such that A5: ( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) ) ; ::_thesis: p in dom Euclide-Function [p,((dl. 0) .--> (x gcd y))] in Euclide-Function by A5, Def2; hence p in dom Euclide-Function by FUNCT_1:1; ::_thesis: verum end; theorem Th9: :: AMI_4:9 for i, j being Integer st i > 0 & j > 0 holds Euclide-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j) proof let i, j be Integer; ::_thesis: ( i > 0 & j > 0 implies Euclide-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j) ) assume ( i > 0 & j > 0 ) ; ::_thesis: Euclide-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j) then [(((dl. 0),(dl. 1)) --> (i,j)),((dl. 0) .--> (i gcd j))] in Euclide-Function by Def2; hence Euclide-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j) by FUNCT_1:1; ::_thesis: verum end; registration cluster Euclide-Algorithm -> NAT -defined the InstructionsF of SCM -valued finite ; coherence Euclide-Algorithm is the InstructionsF of SCM -valued ; end; registration cluster Euclide-Algorithm -> NAT -defined the InstructionsF of SCM -valued finite non halt-free ; coherence not Euclide-Algorithm is halt-free proof 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 Euclide-Algorithm by FUNCT_4:18; then halt SCM in rng Euclide-Algorithm by A4; hence not Euclide-Algorithm is halt-free by COMPOS_1:def_11; ::_thesis: verum end; end; theorem :: AMI_4:10 Euclide-Algorithm , Start-At (0,SCM) computes Euclide-Function proof set q = Euclide-Algorithm ; set p = Start-At (0,SCM); let x be set ; :: according to EXTPRO_1:def_14 ::_thesis: ( not x in dom Euclide-Function or ex b1 being set st ( x = b1 & (Start-At (0,SCM)) +* b1 is Autonomy of Euclide-Algorithm & Euclide-Function . b1 c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* b1)) ) ) DataPart (Start-At (0,SCM)) = {} by MEMSTR_0:20; then A1: dom (DataPart (Start-At (0,SCM))) = {} ; assume x in dom Euclide-Function ; ::_thesis: ex b1 being set st ( x = b1 & (Start-At (0,SCM)) +* b1 is Autonomy of Euclide-Algorithm & Euclide-Function . b1 c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* b1)) ) then consider i1, i2 being Integer such that A2: i1 > 0 and A3: i2 > 0 and A4: x = ((dl. 0),(dl. 1)) --> (i1,i2) by Th8; x = ((dl. 0) .--> i1) +* ((dl. 1) .--> i2) by A4; then reconsider d = x as FinPartState of SCM ; consider t being State of SCM such that A5: (Start-At (0,SCM)) +* d c= t by PBOOLE:141; consider T being Instruction-Sequence of SCM such that A6: Euclide-Algorithm c= T by PBOOLE:145; A7: dom d = {(dl. 0),(dl. 1)} by A4, FUNCT_4:62; then A8: dl. 1 in dom d by TARSKI:def_2; A9: dl. 0 in dom d by A7, TARSKI:def_2; A10: for t being State of SCM st (Start-At (0,SCM)) +* d c= t holds ( t . (dl. 0) = i1 & t . (dl. 1) = i2 ) proof let t be State of SCM; ::_thesis: ( (Start-At (0,SCM)) +* d c= t implies ( t . (dl. 0) = i1 & t . (dl. 1) = i2 ) ) assume A11: (Start-At (0,SCM)) +* d c= t ; ::_thesis: ( t . (dl. 0) = i1 & t . (dl. 1) = i2 ) d c= (Start-At (0,SCM)) +* d by FUNCT_4:25; then A12: d c= t by A11, XBOOLE_1:1; hence t . (dl. 0) = d . (dl. 0) by A9, GRFUNC_1:2 .= i1 by A4, AMI_3:10, FUNCT_4:63 ; ::_thesis: t . (dl. 1) = i2 thus t . (dl. 1) = d . (dl. 1) by A8, A12, GRFUNC_1:2 .= i2 by A4, FUNCT_4:63 ; ::_thesis: verum end; A13: dom (Start-At (0,SCM)) = {(IC )} by FUNCOP_1:13; A14: now__::_thesis:_not_dom_(Start-At_(0,SCM))_meets_dom_d assume dom (Start-At (0,SCM)) meets dom d ; ::_thesis: contradiction then consider x being set such that A15: x in dom (Start-At (0,SCM)) and A16: x in dom d by XBOOLE_0:3; A17: ( x = IC or x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) by A13, A15, TARSKI:def_1; ( x = dl. 0 or x = dl. 1 ) by A7, A16, TARSKI:def_2; hence contradiction by A17, AMI_3:12, AMI_3:13; ::_thesis: verum end; then A18: Start-At (0,SCM) c= (Start-At (0,SCM)) +* d by FUNCT_4:32; A19: IC in dom (Start-At (0,SCM)) by A13, TARSKI:def_1; (dom (Start-At (0,SCM))) /\ (dom d) = {} by A14, XBOOLE_0:def_7; then A20: not IC in dom d by A19, XBOOLE_0:def_4; set A = {(IC ),(dl. 0),(dl. 1)}; set C = 5; A21: dom ((Start-At (0,SCM)) +* d) = dom ((Start-At (0,SCM)) +* d) .= (dom (Start-At (0,SCM))) \/ (dom d) by FUNCT_4:def_1 .= ({(IC )} \/ (dom (DataPart (Start-At (0,SCM))))) \/ (dom d) by A19, MEMSTR_0:24 .= {(IC )} \/ {(dl. 0),(dl. 1)} by A4, A1, FUNCT_4:62 .= {(IC ),(dl. 0),(dl. 1)} by ENUMSET1:2 ; A22: dom (Start-At (0,SCM)) c= dom ((Start-At (0,SCM)) +* d) by A18, RELAT_1:11; IC ((Start-At (0,SCM)) +* d) = IC (Start-At (0,SCM)) by A20, FUNCT_4:11 .= 0 by FUNCOP_1:72 ; then A23: (Start-At (0,SCM)) +* d is 0 -started by A22, A19, MEMSTR_0:def_11; then A24: t is 0 -started by A5, MEMSTR_0:17; A25: (Start-At (0,SCM)) +* d is Euclide-Algorithm -autonomic proof set A = {(IC ),(dl. 0),(dl. 1)}; set C = 5; let P, Q be Instruction-Sequence of SCM; :: according to EXTPRO_1:def_10 ::_thesis: ( not Euclide-Algorithm c= P or not Euclide-Algorithm c= Q or for b1, b2 being set holds ( not (Start-At (0,SCM)) +* d c= b1 or not (Start-At (0,SCM)) +* d c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,b2,b3)) | (dom ((Start-At (0,SCM)) +* d)) ) ) assume that A26: Euclide-Algorithm c= P and A27: Euclide-Algorithm c= Q ; ::_thesis: for b1, b2 being set holds ( not (Start-At (0,SCM)) +* d c= b1 or not (Start-At (0,SCM)) +* d c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,b2,b3)) | (dom ((Start-At (0,SCM)) +* d)) ) let s1, s2 be State of SCM; ::_thesis: ( not (Start-At (0,SCM)) +* d c= s1 or not (Start-At (0,SCM)) +* d c= s2 or for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b1)) | (dom ((Start-At (0,SCM)) +* d)) ) assume that A28: (Start-At (0,SCM)) +* d c= s1 and A29: (Start-At (0,SCM)) +* d c= s2 ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b1)) | (dom ((Start-At (0,SCM)) +* d)) A30: ( s2 . (dl. 0) = i1 & s2 . (dl. 1) = i2 ) by A10, A29; let k be Element of NAT ; ::_thesis: (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d)) defpred S2[ Element of NAT ] means ( IC (Comput (P,s1,\$1)) = IC (Comput (Q,s2,\$1)) & (Comput (P,s1,\$1)) . (dl. 0) = (Comput (Q,s2,\$1)) . (dl. 0) & (Comput (P,s1,\$1)) . (dl. 1) = (Comput (Q,s2,\$1)) . (dl. 1) ); A31: ( Comput (P,s1,0) = s1 & Comput (Q,s2,0) = s2 ) by EXTPRO_1:2; A32: s1 is 0 -started by A23, A28, MEMSTR_0:17; A33: dom (Comput (P,s1,k)) = the carrier of SCM by PARTFUN1:def_2 .= dom (Comput (Q,s2,k)) by PARTFUN1:def_2 ; A34: s2 is 0 -started by A23, A29, MEMSTR_0:17; A35: for i, j being Nat st S2[4 * i] & j <> 0 & j <= 4 holds S2[(4 * i) + j] proof let i, j be Nat; ::_thesis: ( S2[4 * i] & j <> 0 & j <= 4 implies S2[(4 * i) + j] ) assume that A36: IC (Comput (P,s1,(4 * i))) = IC (Comput (Q,s2,(4 * i))) and A37: (Comput (P,s1,(4 * i))) . (dl. 0) = (Comput (Q,s2,(4 * i))) . (dl. 0) and A38: (Comput (P,s1,(4 * i))) . (dl. 1) = (Comput (Q,s2,(4 * i))) . (dl. 1) ; ::_thesis: ( not j <> 0 or not j <= 4 or S2[(4 * i) + j] ) A39: i in NAT by ORDINAL1:def_12; assume ( j <> 0 & j <= 4 ) ; ::_thesis: S2[(4 * i) + j] then A40: ( j = 1 or j = 2 or j = 3 or j = 4 ) by NAT_1:28; percases ( IC (Comput (Q,s2,(4 * i))) = 0 or IC (Comput (Q,s2,(4 * i))) = 4 ) by A2, A3, A34, A27, A30, A39, Lm4; supposeA41: IC (Comput (Q,s2,(4 * i))) = 0 ; ::_thesis: S2[(4 * i) + j] A42: (Comput (P,s1,((4 * i) + 1))) . (dl. 0) = (Comput (P,s1,(4 * i))) . (dl. 0) by A26, A36, A41, Th2 .= (Comput (Q,s2,((4 * i) + 1))) . (dl. 0) by A27, A37, A41, Th2 ; A43: (Comput (P,s1,((4 * i) + 1))) . (dl. 2) = (Comput (P,s1,(4 * i))) . (dl. 1) by A26, A36, A41, Th2 .= (Comput (Q,s2,((4 * i) + 1))) . (dl. 2) by A27, A38, A41, Th2 ; A44: (Comput (P,s1,((4 * i) + 1))) . (dl. 1) = (Comput (P,s1,(4 * i))) . (dl. 1) by A26, A36, A41, Th2 .= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) by A27, A38, A41, Th2 ; A45: ((4 * i) + 1) + 1 = (4 * i) + (1 + 1) ; A46: ((4 * i) + 2) + 1 = (4 * i) + (2 + 1) ; A47: IC (Comput (Q,s2,((4 * i) + 1))) = 1 by A27, A41, Th2; then A48: IC (Comput (Q,s2,((4 * i) + 2))) = 2 by A27, A45, Th3; then A49: IC (Comput (Q,s2,((4 * i) + 3))) = 3 by A27, A46, Th4; A50: IC (Comput (P,s1,((4 * i) + 1))) = 1 by A26, A36, A41, Th2; then A51: (Comput (P,s1,((4 * i) + 2))) . (dl. 2) = (Comput (P,s1,((4 * i) + 1))) . (dl. 2) by A26, A45, Th3 .= (Comput (Q,s2,((4 * i) + 2))) . (dl. 2) by A27, A45, A47, A43, Th3 ; A52: (Comput (P,s1,((4 * i) + 2))) . (dl. 1) = ((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) mod ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3 .= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) by A27, A45, A47, A42, A44, Th3 ; A53: IC (Comput (P,s1,((4 * i) + 2))) = 2 by A26, A45, A50, Th3; then A54: IC (Comput (P,s1,((4 * i) + 3))) = 3 by A26, A46, Th4; A55: (Comput (P,s1,((4 * i) + 2))) . (dl. 0) = ((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) div ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3 .= (Comput (Q,s2,((4 * i) + 2))) . (dl. 0) by A27, A45, A47, A42, A44, Th3 ; A56: ((4 * i) + 3) + 1 = (4 * i) + (3 + 1) ; A57: (Comput (P,s1,((4 * i) + 3))) . (dl. 0) = (Comput (P,s1,((4 * i) + 2))) . (dl. 2) by A26, A46, A53, Th4 .= (Comput (Q,s2,((4 * i) + 3))) . (dl. 0) by A27, A46, A48, A51, Th4 ; A58: (Comput (P,s1,((4 * i) + 3))) . (dl. 1) = (Comput (P,s1,((4 * i) + 2))) . (dl. 1) by A26, A46, A53, Th4 .= (Comput (Q,s2,((4 * i) + 3))) . (dl. 1) by A27, A46, A48, A52, Th4 ; ( (Comput (P,s1,((4 * i) + 3))) . (dl. 1) <= 0 or (Comput (P,s1,((4 * i) + 3))) . (dl. 1) > 0 ) ; then ( ( IC (Comput (P,s1,((4 * i) + 4))) = 4 & IC (Comput (Q,s2,((4 * i) + 4))) = 4 ) or ( IC (Comput (P,s1,((4 * i) + 4))) = 0 & IC (Comput (Q,s2,((4 * i) + 4))) = 0 ) ) by A26, A27, A56, A54, A49, A58, Th5; hence IC (Comput (P,s1,((4 * i) + j))) = IC (Comput (Q,s2,((4 * i) + j))) by A40, A50, A27, A41, Th2, A26, A45, Th3, A48, A54, A46, Th4; ::_thesis: ( (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) & (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) ) (Comput (P,s1,((4 * i) + 4))) . (dl. 0) = (Comput (P,s1,((4 * i) + 3))) . (dl. 0) by A26, A56, A54, Th5 .= (Comput (Q,s2,((4 * i) + 4))) . (dl. 0) by A27, A56, A49, A57, Th5 ; hence (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) by A40, A42, A55, A57; ::_thesis: (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) (Comput (P,s1,((4 * i) + 4))) . (dl. 1) = (Comput (P,s1,((4 * i) + 3))) . (dl. 1) by A26, A56, A54, Th5 .= (Comput (Q,s2,((4 * i) + 4))) . (dl. 1) by A27, A56, A49, A58, Th5 ; hence (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) by A40, A44, A52, A58; ::_thesis: verum end; supposeA59: IC (Comput (Q,s2,(4 * i))) = 4 ; ::_thesis: S2[(4 * i) + j] then P halts_at IC (Comput (P,s1,(4 * i))) by A26, A36, Lm3; then A60: Comput (P,s1,((4 * i) + j)) = Comput (P,s1,(4 * i)) by EXTPRO_1:20, NAT_1:11; Q halts_at IC (Comput (Q,s2,(4 * i))) by A27, A59, Lm3; hence S2[(4 * i) + j] by A36, A37, A38, A60, EXTPRO_1:20, NAT_1:11; ::_thesis: verum end; end; end; (Comput (P,s1,0)) . (IC ) = IC s1 by EXTPRO_1:2 .= 0 by A32, MEMSTR_0:def_11 .= IC s2 by A34, MEMSTR_0:def_11 .= (Comput (Q,s2,0)) . (IC ) by EXTPRO_1:2 ; then A61: S2[ 0 ] by A10, A28, A30, A31; A62: 4 > 0 ; S2[k] from NAT_D:sch_2(A61, A62, A35); hence (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d)) by A21, A33, GRFUNC_1:31; ::_thesis: verum end; take d ; ::_thesis: ( x = d & (Start-At (0,SCM)) +* d is Autonomy of Euclide-Algorithm & Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) ) thus x = d ; ::_thesis: ( (Start-At (0,SCM)) +* d is Autonomy of Euclide-Algorithm & Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) ) A63: (Start-At (0,SCM)) +* d is Euclide-Algorithm -halted proof reconsider i19 = i1, i29 = i2 as Element of NAT by A2, A3, INT_1:3; let t be State of SCM; :: according to EXTPRO_1:def_11 ::_thesis: ( not (Start-At (0,SCM)) +* d c= t or for b1 being set holds ( not Euclide-Algorithm c= b1 or b1 halts_on t ) ) assume A64: (Start-At (0,SCM)) +* d c= t ; ::_thesis: for b1 being set holds ( not Euclide-Algorithm c= b1 or b1 halts_on t ) let P be Instruction-Sequence of SCM; ::_thesis: ( not Euclide-Algorithm c= P or P halts_on t ) assume A65: Euclide-Algorithm c= P ; ::_thesis: P halts_on t set t9 = Comput (P,t,4); A66: t . (dl. 1) = i2 by A10, A64; A67: ( t is 0 -started & t . (dl. 0) = i1 ) by A23, A10, A64, MEMSTR_0:17; percases ( i1 > i2 or i1 = i2 or i1 < i2 ) by XXREAL_0:1; suppose i1 > i2 ; ::_thesis: P halts_on t then ex k being Element of NAT st P halts_at IC (Comput (P,t,k)) by A3, A65, A67, A66, Lm6; hence P halts_on t by EXTPRO_1:16; ::_thesis: verum end; supposeA68: i1 = i2 ; ::_thesis: P halts_on t A69: i1 mod i2 = i19 mod i29 .= 0 by A68, NAT_D:25 ; A70: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ; t = Comput (P,t,(4 * 0)) by EXTPRO_1:2; then (Comput (P,t,4)) . (dl. 1) = (t . (dl. 0)) mod (t . (dl. 1)) by A2, A3, A65, A67, A66, A70, Lm5; then IC (Comput (P,t,4)) = 4 by A2, A3, A65, A67, A66, A69, A70, Lm4; then P halts_at IC (Comput (P,t,4)) by A65, Lm3; hence P halts_on t by EXTPRO_1:16; ::_thesis: verum end; supposeA71: i1 < i2 ; ::_thesis: P halts_on t A72: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ; A73: t = Comput (P,t,(4 * 0)) by EXTPRO_1:2; i1 mod i2 = i19 mod i29 .= i19 by A71, NAT_D:24 ; then A74: (Comput (P,t,4)) . (dl. 1) = i1 by A2, A3, A65, A67, A66, A73, A72, Lm5; then IC (Comput (P,t,4)) = 0 by A2, A3, A65, A67, A66, A72, Lm4; then A75: Comput (P,t,4) is 0 -started by MEMSTR_0:def_12; (Comput (P,t,4)) . (dl. 0) = i2 by A2, A3, A65, A67, A66, A73, A72, Lm5; then consider k0 being Element of NAT such that A76: P halts_at IC (Comput (P,(Comput (P,t,4)),k0)) by A2, A71, A74, A75, A65, Lm6; P halts_at IC (Comput (P,t,(k0 + 4))) by A76, EXTPRO_1:4; hence P halts_on t by EXTPRO_1:16; ::_thesis: verum end; end; end; thus (Start-At (0,SCM)) +* d is Autonomy of Euclide-Algorithm by A25, A63, EXTPRO_1:def_12; ::_thesis: Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) then A77: Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) = (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A6, A5, EXTPRO_1:def_13; dl. 0 in the carrier of SCM ; then A78: dl. 0 in dom (Result (T,t)) by PARTFUN1:def_2; A79: d . (dl. 0) = i1 by A4, AMI_3:10, FUNCT_4:63; A80: d . (dl. 1) = i2 by A4, FUNCT_4:63; A81: d c= (Start-At (0,SCM)) +* d by FUNCT_4:25; A82: dom d c= dom ((Start-At (0,SCM)) +* d) by A81, RELAT_1:11; A83: d c= t by A81, A5, XBOOLE_1:1; A84: dom d = {(dl. 0),(dl. 1)} by A4, FUNCT_4:62; then A85: dl. 1 in dom d by TARSKI:def_2; A86: t . (dl. 1) = i2 by A83, A80, A85, GRFUNC_1:2; A87: dl. 0 in dom d by A84, TARSKI:def_2; t . (dl. 0) = i1 by A83, A79, A87, GRFUNC_1:2; then A88: (Result (T,t)) . (dl. 0) = i1 gcd i2 by A2, A3, A24, A86, Th7, A6; A89: dom ((dl. 0) .--> (i1 gcd i2)) = {(dl. 0)} by FUNCOP_1:13; dom ((dl. 0) .--> (i1 gcd i2)) c= dom d by A84, A89, ZFMISC_1:7; then A90: dom ((dl. 0) .--> (i1 gcd i2)) c= dom ((Start-At (0,SCM)) +* d) by A82, XBOOLE_1:1; (dl. 0) .--> (i1 gcd i2) c= (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A90, A78, A88, FUNCT_4:85, RELAT_1:151; hence Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) by A77, A2, A3, A4, Th9; ::_thesis: verum end;