:: 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;