:: AMI_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: AMI_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Integer st i >= 0 & j >= 0 holds
i div j >= 0
proof end;

theorem Th2: :: AMI_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Integer st i >= 0 & j >= 0 holds
( (abs i) mod (abs j) = i mod j & (abs i) div (abs j) = i div j )
proof end;

scheme :: AMI_4:sch 1
Euklides'{ F1( Nat) -> Nat, F2( Nat) -> Nat, F3() -> Nat, F4() -> Nat } :
ex k being Nat st
( F1(k) = F3() hcf F4() & F2(k) = 0 )
provided
A1: 0 < F4() and
A2: F4() < F3() and
A3: F1(0) = F3() and
A4: F2(0) = F4() and
A5: for k being Nat st F2(k) > 0 holds
( F1((k + 1)) = F2(k) & F2((k + 1)) = F1(k) mod F2(k) )
proof end;

set a = dl. 0;

set b = dl. 1;

set c = 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 end;
correctness
;
end;

:: deftheorem 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 ( $1 . (il. 0) = (dl. 2) := (dl. 1) & $1 . (il. 1) = Divide (dl. 0),(dl. 1) & $1 . (il. 2) = (dl. 0) := (dl. 2) & $1 . (il. 3) = (dl. 1) >0_goto (il. 0) & $1 halts_at il. 4 );

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

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

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

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

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

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

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

set EA1 = ((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 EA0 = ((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 :: AMI_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: AMI_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
dom Euclide-Algorithm = {(il. 0),(il. 1),(il. 2),(il. 3),(il. 4)}
proof end;

Lm1: for s being State of SCM st Euclide-Algorithm c= s holds
S1[s]
proof end;

theorem Th5: :: AMI_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM st Euclide-Algorithm c= s holds
for k being Nat st IC ((Computation s) . k) = il. 0 holds
( IC ((Computation s) . (k + 1)) = il. 1 & ((Computation s) . (k + 1)) . (dl. 0) = ((Computation s) . k) . (dl. 0) & ((Computation s) . (k + 1)) . (dl. 1) = ((Computation s) . k) . (dl. 1) & ((Computation s) . (k + 1)) . (dl. 2) = ((Computation s) . k) . (dl. 1) )
proof end;

theorem Th6: :: AMI_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM st Euclide-Algorithm c= s holds
for k being Nat st IC ((Computation s) . k) = il. 1 holds
( IC ((Computation s) . (k + 1)) = il. 2 & ((Computation s) . (k + 1)) . (dl. 0) = (((Computation s) . k) . (dl. 0)) div (((Computation s) . k) . (dl. 1)) & ((Computation s) . (k + 1)) . (dl. 1) = (((Computation s) . k) . (dl. 0)) mod (((Computation s) . k) . (dl. 1)) & ((Computation s) . (k + 1)) . (dl. 2) = ((Computation s) . k) . (dl. 2) )
proof end;

theorem Th7: :: AMI_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM st Euclide-Algorithm c= s holds
for k being Nat st IC ((Computation s) . k) = il. 2 holds
( IC ((Computation s) . (k + 1)) = il. 3 & ((Computation s) . (k + 1)) . (dl. 0) = ((Computation s) . k) . (dl. 2) & ((Computation s) . (k + 1)) . (dl. 1) = ((Computation s) . k) . (dl. 1) & ((Computation s) . (k + 1)) . (dl. 2) = ((Computation s) . k) . (dl. 2) )
proof end;

theorem Th8: :: AMI_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM st Euclide-Algorithm c= s holds
for k being Nat st IC ((Computation s) . k) = il. 3 holds
( ( ((Computation s) . k) . (dl. 1) > 0 implies IC ((Computation s) . (k + 1)) = il. 0 ) & ( ((Computation s) . k) . (dl. 1) <= 0 implies IC ((Computation s) . (k + 1)) = il. 4 ) & ((Computation s) . (k + 1)) . (dl. 0) = ((Computation s) . k) . (dl. 0) & ((Computation s) . (k + 1)) . (dl. 1) = ((Computation s) . k) . (dl. 1) )
proof end;

theorem Th9: :: AMI_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM st Euclide-Algorithm c= s holds
for k, i being Nat st IC ((Computation s) . k) = il. 4 holds
(Computation s) . (k + i) = (Computation s) . k
proof end;

Lm2: for k being Nat
for s being State of SCM st s starts_at il. 0 & Euclide-Algorithm c= s & s . (dl. 0) > 0 & s . (dl. 1) > 0 holds
( ((Computation s) . (4 * k)) . (dl. 0) > 0 & ( ( ((Computation s) . (4 * k)) . (dl. 1) > 0 & IC ((Computation s) . (4 * k)) = il. 0 ) or ( ((Computation s) . (4 * k)) . (dl. 1) = 0 & IC ((Computation s) . (4 * k)) = il. 4 ) ) )
proof end;

Lm3: for k being Nat
for s being State of SCM st s starts_at il. 0 & Euclide-Algorithm c= s & s . (dl. 0) > 0 & s . (dl. 1) > 0 & ((Computation s) . (4 * k)) . (dl. 1) > 0 holds
( ((Computation s) . (4 * (k + 1))) . (dl. 0) = ((Computation s) . (4 * k)) . (dl. 1) & ((Computation s) . (4 * (k + 1))) . (dl. 1) = (((Computation s) . (4 * k)) . (dl. 0)) mod (((Computation s) . (4 * k)) . (dl. 1)) )
proof end;

Lm4: for s being State of SCM st s starts_at il. 0 & Euclide-Algorithm c= s holds
for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds
( (Result s) . (dl. 0) = x gcd y & ex k being Nat st s halts_at IC ((Computation s) . k) )
proof end;

theorem Th10: :: AMI_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM st s starts_at il. 0 & Euclide-Algorithm c= s holds
for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 holds
(Result s) . (dl. 0) = x gcd y
proof 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 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 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 Th11: :: AMI_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th12: :: AMI_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: AMI_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
(Start-At (il. 0)) +* Euclide-Algorithm computes Euclide-Function
proof end;