:: AMI_4 semantic presentation

theorem Th1: :: AMI_4:1
for b1, b2 being Integer holds
( b1 >= 0 & b2 >= 0 implies b1 div b2 >= 0 )
proof
let c1, c2 be Integer;
assume E2: ( c1 >= 0 & c2 >= 0 ) ;
E3: c1 div c2 = [\(c1 / c2)/] by INT_1:def 7;
E4: (c1 / c2) - 1 < [\(c1 / c2)/] by INT_1:def 4;
( c1 / c2 >= 0 & 0 - 1 = - 1 ) by E2, REAL_2:125;
then (c1 / c2) - 1 >= - 1 by XREAL_1:11;
then - 1 < [\(c1 / c2)/] by E4, XXREAL_0:2;
hence c1 div c2 >= 0 by E3, INT_1:21;
end;

theorem Th2: :: AMI_4:2
for b1, b2 being Integer holds
( b1 >= 0 & b2 >= 0 implies ( (abs b1) mod (abs b2) = b1 mod b2 & (abs b1) div (abs b2) = b1 div b2 ) )
proof
let c1, c2 be Integer;
assume that
E3: c1 >= 0 and
E4: c2 >= 0 ;
per cases not ( not c2 > 0 & not c2 = 0 ) by E4;
suppose E5: c2 > 0 ;
then E6: ( c1 = abs c1 & c2 = abs c2 ) by E3, ABSVALUE:def 1;
( c1 mod c2 >= 0 & c1 div c2 >= 0 ) by E3, E5, Th1, NEWTON:78;
then reconsider c3 = c1 mod c2, c4 = c1 div c2 as Nat by INT_1:16;
E7: c3 < c2 by E5, NEWTON:79;
c3 = c1 - (c4 * c2) by E5, INT_1:def 8;
then c1 = (c2 * c4) + c3 ;
hence ( (abs c1) mod (abs c2) = c1 mod c2 & (abs c1) div (abs c2) = c1 div c2 ) by E6, E7, NAT_1:def 1, NAT_1:def 2;
end;
suppose E5: c2 = 0 ;
abs 0 = 0 by ABSVALUE:def 1;
then ( (abs c1) mod (abs 0) = 0 & (abs c1) div (abs 0) = 0 ) by NAT_1:def 1, NAT_1:def 2;
hence ( (abs c1) mod (abs c2) = c1 mod c2 & (abs c1) div (abs c2) = c1 div c2 ) by E5, INT_1:75, INT_1:def 8;
end;
end;
end;

scheme :: AMI_4:sch 1
s1{ F1( Nat) -> Nat, F2( Nat) -> Nat, F3() -> Nat, F4() -> Nat } :
ex b1 being Nat st
( F1(b1) = F3() hcf F4() & F2(b1) = 0 )
provided
E3: 0 < F4() and E4: F4() < F3() and E5: F1(0) = F3() and E6: F2(0) = F4() and E7: for b1 being Nat holds
( F2(b1) > 0 implies ( F1((b1 + 1)) = F2(b1) & F2((b1 + 1)) = F1(b1) mod F2(b1) ) )
proof
E8: ( 0 < F4() & F4() < F3() ) by E3, E4;
deffunc H1( Nat, set ) -> M2( NAT ) = IFEQ a2,0,0,F2(a1);
consider c1 being Function of NAT , NAT such that
E9: c1 . 0 = F3() and
E10: for b1 being Nat holds c1 . (b1 + 1) = H1(b1,c1 . b1) from RECDEF_1:sch 4();
 deffunc H2( Nat) -> M2( NAT ) = c1 . a1;
c1 . (0 + 1) = IFEQ (c1 . 0),0,0,F2(0) by E10
.= F2(0) by E4, E9, CQC_LANG:def 1 ;
then E11: ( H2(0) = F3() & H2(1) = F4() ) by E6, E9;
E12: for b1 being Nat holds
( c1 . b1 > 0 implies c1 . b1 = F1(b1) )
proof
let c2 be Nat;
assume E13: c1 . c2 > 0 ;
now
per cases not ( not c2 = 0 & not c2 <> 0 ) ;
case c2 = 0 ;
hence c1 . c2 = F1(c2) by E5, E9;
end;
case c2 <> 0 ;
then consider c3 being Nat such that
E14: c2 = c3 + 1 by NAT_1:22;
E15: now
assume E16: c1 . c3 = 0 ;
c1 . c2 = IFEQ (c1 . c3),0,0,F2(c3) by E10, E14
.= 0 by E16, CQC_LANG:def 1 ;
hence not verum by E13;
end;
c1 . c2 = IFEQ (c1 . c3),0,0,F2(c3) by E10, E14
.= F2(c3) by E15, CQC_LANG:def 1 ;
hence c1 . c2 = F1(c2) by E7, E13, E14;
end;
end;
end;
hence c1 . c2 = F1(c2) ;
end;
E13: for b1 being Nat holds H2(b1 + 2) = H2(b1) mod H2(b1 + 1)
proof
let c2 be Nat;
now
per cases not ( not c1 . (c2 + 1) <> 0 & not c1 . (c2 + 1) = 0 ) ;
case E14: c1 . (c2 + 1) <> 0 ;
now
assume E15: F2(c2) = 0 ;
E16: not ( not c1 . c2 = 0 & not c1 . c2 <> 0 ) ;
c1 . (c2 + 1) = IFEQ (c1 . c2),0,0,F2(c2) by E10
.= 0 by E15, E16, CQC_LANG:def 1 ;
hence not verum by E14;
end;
then E15: F2(c2) > 0 ;
E16: c1 . (c2 + (1 + 1)) = c1 . ((c2 + 1) + 1)
.= IFEQ (c1 . (c2 + 1)),0,0,F2((c2 + 1)) by E10
.= F2((c2 + 1)) by E14, CQC_LANG:def 1
.= F1(c2) mod F2(c2) by E7, E15 ;
E17: now
assume E18: c1 . c2 = 0 ;
c1 . (c2 + 1) = IFEQ (c1 . c2),0,0,F2(c2) by E10
.= 0 by E18, CQC_LANG:def 1 ;
hence not verum by E14;
end;
then E18: c1 . c2 > 0 ;
c1 . (c2 + 1) = IFEQ (c1 . c2),0,0,F2(c2) by E10
.= F2(c2) by E17, CQC_LANG:def 1 ;
hence c1 . (c2 + 2) = (c1 . c2) mod (c1 . (c2 + 1)) by E12, E16, E18;
end;
case E14: c1 . (c2 + 1) = 0 ;
thus c1 . (c2 + 2) = c1 . ((c2 + 1) + 1)
.= IFEQ (c1 . (c2 + 1)),0,0,F2((c2 + 1)) by E10
.= 0 by E14, CQC_LANG:def 1
.= (c1 . c2) mod (c1 . (c2 + 1)) by E14, NAT_1:def 2 ;
end;
end;
end;
hence c1 . (c2 + 2) = (c1 . c2) mod (c1 . (c2 + 1)) ;
end;
consider c2 being Nat such that
E14: ( H2(c2) = F3() hcf F4() & H2(c2 + 1) = 0 ) from NAT_1:sch 8(E8, E11, E13);
 take c2 ;
E15: F3() hcf F4() > 0 by E3, NEWTON:71;
hence F1(c2) = F3() hcf F4() by E12, E14;
thus F2(c2) = IFEQ (c1 . c2),0,0,F2(c2) by E14, E15, CQC_LANG:def 1
.= 0 by E10, E14 ;
end;

set c1 = dl. 0;

set c2 = dl. 1;

set c3 = dl. 2;

definition
func Euclide-Algorithm -> programmed FinPartState of SCM equals :: AMI_4:def 1
((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))));
coherence
((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) is programmed FinPartState of SCM
proof
set c4 = ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ));
set c5 = ((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )));
((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )) is programmed by AMI_3:35;
then ((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) is programmed by AMI_3:35;
then ((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) is programmed by AMI_3:35;
hence ((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) is programmed FinPartState of SCM by AMI_3:35;
end;
correctness
;
end;

:: deftheorem Def1 defines Euclide-Algorithm AMI_4:def 1 :
Euclide-Algorithm = ((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))));

defpred S1[ State of SCM ] means ( a1 . (il. 0) = (dl. 2) := (dl. 1) & a1 . (il. 1) = Divide (dl. 0),(dl. 1) & a1 . (il. 2) = (dl. 0) := (dl. 2) & a1 . (il. 3) = (dl. 1) >0_goto (il. 0) & a1 halts_at il. 4 );

set c4 = (il. 0) .--> ((dl. 2) := (dl. 1));

set c5 = (il. 1) .--> (Divide (dl. 0),(dl. 1));

set c6 = (il. 2) .--> ((dl. 0) := (dl. 2));

set c7 = (il. 3) .--> ((dl. 1) >0_goto (il. 0));

set c8 = (il. 4) .--> (halt SCM );

set c9 = ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ));

set c10 = ((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )));

set c11 = ((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))));

set c12 = ((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))));

theorem Th3: :: AMI_4:3
canceled;

theorem Th4: :: AMI_4:4
dom Euclide-Algorithm = {(il. 0),(il. 1),(il. 2),(il. 3),(il. 4)}
proof
E4: dom ((il. 0) .--> ((dl. 2) := (dl. 1))) = {(il. 0)} by CQC_LANG:5;
E5: dom ((il. 1) .--> (Divide (dl. 0),(dl. 1))) = {(il. 1)} by CQC_LANG:5;
E6: dom ((il. 2) .--> ((dl. 0) := (dl. 2))) = {(il. 2)} by CQC_LANG:5;
E7: dom ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) = {(il. 3)} by CQC_LANG:5;
dom ((il. 4) .--> (halt SCM )) = {(il. 4)} by CQC_LANG:5;
then dom (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) = {(il. 3)} \/ {(il. 4)} by E7, FUNCT_4:def 1
.= {(il. 3),(il. 4)} by ENUMSET1:41 ;
then dom (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) = {(il. 2)} \/ {(il. 3),(il. 4)} by E6, FUNCT_4:def 1
.= {(il. 2),(il. 3),(il. 4)} by ENUMSET1:42 ;
then dom (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) = {(il. 1)} \/ {(il. 2),(il. 3),(il. 4)} by E5, FUNCT_4:def 1
.= {(il. 1),(il. 2),(il. 3),(il. 4)} by ENUMSET1:44 ;
then dom (((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))))) = {(il. 0)} \/ {(il. 1),(il. 2),(il. 3),(il. 4)} by E4, FUNCT_4:def 1
.= {(il. 0),(il. 1),(il. 2),(il. 3),(il. 4)} by ENUMSET1:47 ;
hence dom Euclide-Algorithm = {(il. 0),(il. 1),(il. 2),(il. 3),(il. 4)} ;
end;

Lemma4: for b1 being State of SCM holds
( Euclide-Algorithm c= b1 implies S1[b1] )
proof
let c13 be State of SCM ;
E5: dom ((il. 1) .--> (Divide (dl. 0),(dl. 1))) = {(il. 1)} by CQC_LANG:5;
E6: dom ((il. 2) .--> ((dl. 0) := (dl. 2))) = {(il. 2)} by CQC_LANG:5;
E7: dom ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) = {(il. 3)} by CQC_LANG:5;
E8: dom ((il. 4) .--> (halt SCM )) = {(il. 4)} by CQC_LANG:5;
then E9: dom (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) = {(il. 3)} \/ {(il. 4)} by E7, FUNCT_4:def 1
.= {(il. 3),(il. 4)} by ENUMSET1:41 ;
then E10: dom (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) = {(il. 2)} \/ {(il. 3),(il. 4)} by E6, FUNCT_4:def 1
.= {(il. 2),(il. 3),(il. 4)} by ENUMSET1:42 ;
then E11: dom (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) = {(il. 1)} \/ {(il. 2),(il. 3),(il. 4)} by E5, FUNCT_4:def 1
.= {(il. 1),(il. 2),(il. 3),(il. 4)} by ENUMSET1:44 ;
assume E12: Euclide-Algorithm c= c13 ;
E13: not il. 0 in dom (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) by E11, ENUMSET1:def 2;
il. 0 in dom (((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))))) by Th4, ENUMSET1:def 3;
hence c13 . (il. 0) = (((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))))) . (il. 0) by E12, GRFUNC_1:8
.= ((il. 0) .--> ((dl. 2) := (dl. 1))) . (il. 0) by E13, FUNCT_4:12
.= (dl. 2) := (dl. 1) by CQC_LANG:6 ;

((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) c= ((il. 0) .--> ((dl. 2) := (dl. 1))) +* (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) by FUNCT_4:26;
then E14: ((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) c= c13 by E12, XBOOLE_1:1;
E15: not il. 1 in dom (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) by E10, ENUMSET1:def 1;
il. 1 in dom (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) by E11, ENUMSET1:def 2;
hence c13 . (il. 1) = (((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))))) . (il. 1) by E14, GRFUNC_1:8
.= ((il. 1) .--> (Divide (dl. 0),(dl. 1))) . (il. 1) by E15, FUNCT_4:12
.= Divide (dl. 0),(dl. 1) by CQC_LANG:6 ;

((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) c= ((il. 1) .--> (Divide (dl. 0),(dl. 1))) +* (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) by FUNCT_4:26;
then E16: ((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) c= c13 by E14, XBOOLE_1:1;
E17: not il. 2 in dom (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) by E9, TARSKI:def 2;
il. 2 in dom (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) by E10, ENUMSET1:def 1;
hence c13 . (il. 2) = (((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )))) . (il. 2) by E16, GRFUNC_1:8
.= ((il. 2) .--> ((dl. 0) := (dl. 2))) . (il. 2) by E17, FUNCT_4:12
.= (dl. 0) := (dl. 2) by CQC_LANG:6 ;

((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )) c= ((il. 2) .--> ((dl. 0) := (dl. 2))) +* (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) by FUNCT_4:26;
then E18: ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM )) c= c13 by E16, XBOOLE_1:1;
E19: not il. 3 in dom ((il. 4) .--> (halt SCM )) by E8, TARSKI:def 1;
il. 3 in dom (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) by E9, TARSKI:def 2;
hence c13 . (il. 3) = (((il. 3) .--> ((dl. 1) >0_goto (il. 0))) +* ((il. 4) .--> (halt SCM ))) . (il. 3) by E18, GRFUNC_1:8
.= ((il. 3) .--> ((dl. 1) >0_goto (il. 0))) . (il. 3) by E19,