set q = Euclide-Algorithm ;
set p = (Start-At (0,SCM)) +* Euclide-Algorithm;
let x be set ; :: according to EXTPRO_1:def 13 :: thesis: ( not x in proj1 Euclide-Function or ex b1 being set st
( x = b1 & ((Start-At (0,SCM)) +* Euclide-Algorithm) +* b1 is Autonomy of ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) & Euclide-Function . b1 c= Result ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* b1)) ) )
A1: ( IC SCM <> 2 & IC SCM <> 3 ) by AMI_3:57;
A2: IC SCM <> 4 by AMI_3:57;
( IC SCM <> 0 & IC SCM <> 1 ) by AMI_3:57;
then A3: not IC SCM in dom Euclide-Algorithm by A1, A2, Th4, CARD_1:91, ENUMSET1:def 3;
assume x in dom Euclide-Function ; :: thesis: ex b1 being set st
( x = b1 & ((Start-At (0,SCM)) +* Euclide-Algorithm) +* b1 is Autonomy of ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) & Euclide-Function . b1 c= Result ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* b1)) )
then consider i1, i2 being Integer such that
A4: i1 > 0 and
A5: i2 > 0 and
A6: x = ((dl. 0),(dl. 1)) --> (i1,i2) by Th11;
reconsider d = x as FinPartState of SCM by A6;
consider t being State of SCM such that
A7: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t by PBOOLE:156;
A8: dom d = {(dl. 0),(dl. 1)} by A6, FUNCT_4:65;
then A9: dl. 1 in dom d by TARSKI:def 2;
A10: dl. 0 in dom d by A8, TARSKI:def 2;
A11: for t being State of SCM st ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t holds
( t . (dl. 0) = i1 & t . (dl. 1) = i2 )
proof
A12: d c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by FUNCT_4:26;
let t be State of SCM; :: thesis: ( ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t implies ( t . (dl. 0) = i1 & t . (dl. 1) = i2 ) )
assume ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t ; :: thesis: ( t . (dl. 0) = i1 & t . (dl. 1) = i2 )
then A13: d c= t by A12, XBOOLE_1:1;
hence t . (dl. 0) = d . (dl. 0) by A10, GRFUNC_1:8
.= i1 by A6, AMI_3:52, FUNCT_4:66 ;
:: thesis: t . (dl. 1) = i2
thus t . (dl. 1) = d . (dl. 1) by A9, A13, GRFUNC_1:8
.= i2 by A6, FUNCT_4:66 ; :: thesis: verum
end;
dom (Start-At (0,SCM)) = {(IC SCM)} by FUNCOP_1:19;
then A14: dom ((Start-At (0,SCM)) +* Euclide-Algorithm) = {(IC SCM)} \/ 5 by Th4, FUNCT_4:def 1;
A15: now
assume dom ((Start-At (0,SCM)) +* Euclide-Algorithm) meets dom d ; :: thesis: contradiction
then consider x being set such that
A16: x in dom ((Start-At (0,SCM)) +* Euclide-Algorithm) and
A17: x in dom d by XBOOLE_0:3;
( x in {(IC SCM)} or x in 5 ) by A14, A16, XBOOLE_0:def 3;
then A18: ( x = IC SCM or x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) by CARD_1:91, ENUMSET1:def 3, TARSKI:def 1;
( x = dl. 0 or x = dl. 1 ) by A8, A17, TARSKI:def 2;
hence contradiction by A18, AMI_3:56, AMI_3:57; :: thesis: verum
end;
then A19: (Start-At (0,SCM)) +* Euclide-Algorithm c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by FUNCT_4:33;
IC SCM in {(IC SCM)} by TARSKI:def 1;
then A20: IC SCM in dom ((Start-At (0,SCM)) +* Euclide-Algorithm) by A14, XBOOLE_0:def 3;
(dom ((Start-At (0,SCM)) +* Euclide-Algorithm)) /\ (dom d) = {} by A15, XBOOLE_0:def 7;
then A21: not IC SCM in dom d by A20, XBOOLE_0:def 4;
A22: dom ((Start-At (0,SCM)) +* Euclide-Algorithm) c= dom (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) by A19, RELAT_1:25;
IC (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) = ((Start-At (0,SCM)) +* Euclide-Algorithm) . (IC SCM) by A21, FUNCT_4:12
.= (Start-At (0,SCM)) . (IC SCM) by A3, FUNCT_4:12
.= 0 by FUNCOP_1:87 ;
then A23: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is 0 -started by A22, A20, COMPOS_1:def 16;
then A24: t is 0 -started by A7, COMPOS_1:8;
Euclide-Algorithm c= (Start-At (0,SCM)) +* Euclide-Algorithm by FUNCT_4:26;
then Euclide-Algorithm c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by A19, XBOOLE_1:1;
then A25: Euclide-Algorithm c= ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) by RELAT_1:210;
A26: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is autonomic
proof
set A = {(IC SCM),(dl. 0),(dl. 1)};
set C = 5;
let s1, s2 be State of SCM; :: according to EXTPRO_1:def 9 :: thesis: ( not ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= s1 or not ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= s2 or for b1 being Element of NAT holds (Comput ((ProgramPart s1),s1,b1)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) = (Comput ((ProgramPart s2),s2,b1)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) )
assume that
A27: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= s1 and
A28: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= s2 ; :: thesis: for b1 being Element of NAT holds (Comput ((ProgramPart s1),s1,b1)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) = (Comput ((ProgramPart s2),s2,b1)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d))
A29: ( s2 . (dl. 0) = i1 & s2 . (dl. 1) = i2 ) by A11, A28;
let k be Element of NAT ; :: thesis: (Comput ((ProgramPart s1),s1,k)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) = (Comput ((ProgramPart s2),s2,k)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d))
B30: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= ProgramPart s2 by A28, RELAT_1:105;
then A30: Euclide-Algorithm c= ProgramPart s2 by A25, XBOOLE_1:1;
defpred S2[ Element of NAT ] means ( (Comput ((ProgramPart s1),s1,$1)) . (IC SCM) = (Comput ((ProgramPart s2),s2,$1)) . (IC SCM) & (Comput ((ProgramPart s1),s1,$1)) . (dl. 0) = (Comput ((ProgramPart s2),s2,$1)) . (dl. 0) & (Comput ((ProgramPart s1),s1,$1)) . (dl. 1) = (Comput ((ProgramPart s2),s2,$1)) . (dl. 1) );
A32: ( Comput ((ProgramPart s1),s1,0) = s1 & Comput ((ProgramPart s2),s2,0) = s2 ) by EXTPRO_1:3;
A33: s1 is 0 -started by A23, A27, COMPOS_1:8;
A34: dom (Comput ((ProgramPart s1),s1,k)) = the carrier of SCM by PARTFUN1:def 4
.= dom (Comput ((ProgramPart s2),s2,k)) by PARTFUN1:def 4 ;
B35: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= ProgramPart s1 by A27, RELAT_1:105;
then A35: Euclide-Algorithm c= ProgramPart s1 by A25, XBOOLE_1:1;
A36: (ProgramPart s1) | 5 = Euclide-Algorithm by Th4, B35, A25, GRFUNC_1:64, XBOOLE_1:1
.= (ProgramPart s2) | 5 by B30, Th4, A25, GRFUNC_1:64, XBOOLE_1:1 ;
A37: s2 is 0 -started by A23, A28, COMPOS_1:8;
A38: 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
A39: (Comput ((ProgramPart s1),s1,(4 * i))) . (IC SCM) = (Comput ((ProgramPart s2),s2,(4 * i))) . (IC SCM) and
A40: (Comput ((ProgramPart s1),s1,(4 * i))) . (dl. 0) = (Comput ((ProgramPart s2),s2,(4 * i))) . (dl. 0) and
A41: (Comput ((ProgramPart s1),s1,(4 * i))) . (dl. 1) = (Comput ((ProgramPart s2),s2,(4 * i))) . (dl. 1) ; :: thesis: ( not j <> 0 or not j <= 4 or S2[(4 * i) + j] )
A42: i in NAT by ORDINAL1:def 13;
assume ( j <> 0 & j <= 4 ) ; :: thesis: S2[(4 * i) + j]
then A43: ( j = 1 or j = 2 or j = 3 or j = 4 ) by NAT_1:29;
per cases ( IC (Comput ((ProgramPart s2),s2,(4 * i))) = 0 or IC (Comput ((ProgramPart s2),s2,(4 * i))) = 4 ) by A4, A5, A37, A30, A29, A42, Lm4;
suppose A44: IC (Comput ((ProgramPart s2),s2,(4 * i))) = 0 ; :: thesis: S2[(4 * i) + j]
then A45: IC (Comput ((ProgramPart s1),s1,(4 * i))) = 0 by A39;
then A46: (Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 0) = (Comput ((ProgramPart s1),s1,(4 * i))) . (dl. 0) by A35, Th5
.= (Comput ((ProgramPart s2),s2,((4 * i) + 1))) . (dl. 0) by A30, A40, A44, Th5 ;
A47: (Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 2) = (Comput ((ProgramPart s1),s1,(4 * i))) . (dl. 1) by A35, A45, Th5
.= (Comput ((ProgramPart s2),s2,((4 * i) + 1))) . (dl. 2) by A30, A41, A44, Th5 ;
A48: (Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 1) = (Comput ((ProgramPart s1),s1,(4 * i))) . (dl. 1) by A35, A45, Th5
.= (Comput ((ProgramPart s2),s2,((4 * i) + 1))) . (dl. 1) by A30, A41, A44, Th5 ;
A49: ((4 * i) + 1) + 1 = (4 * i) + (1 + 1) ;
A50: ((4 * i) + 2) + 1 = (4 * i) + (2 + 1) ;
A51: IC (Comput ((ProgramPart s2),s2,((4 * i) + 1))) = 1 by A30, A44, Th5;
then A52: IC (Comput ((ProgramPart s2),s2,((4 * i) + 2))) = 2 by A30, A49, Th6;
then A53: IC (Comput ((ProgramPart s2),s2,((4 * i) + 3))) = 3 by A30, A50, Th7;
A54: IC (Comput ((ProgramPart s1),s1,((4 * i) + 1))) = 1 by A35, A45, Th5;
then A55: (Comput ((ProgramPart s1),s1,((4 * i) + 2))) . (dl. 2) = (Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 2) by A35, A49, Th6
.= (Comput ((ProgramPart s2),s2,((4 * i) + 2))) . (dl. 2) by A30, A49, A51, A47, Th6 ;
A56: (Comput ((ProgramPart s1),s1,((4 * i) + 2))) . (dl. 1) = ((Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 0)) mod ((Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 1)) by A35, A49, A54, Th6
.= (Comput ((ProgramPart s2),s2,((4 * i) + 2))) . (dl. 1) by A30, A49, A51, A46, A48, Th6 ;
A57: IC (Comput ((ProgramPart s1),s1,((4 * i) + 2))) = 2 by A35, A49, A54, Th6;
then A58: IC (Comput ((ProgramPart s1),s1,((4 * i) + 3))) = 3 by A35, A50, Th7;
A59: (Comput ((ProgramPart s1),s1,((4 * i) + 2))) . (dl. 0) = ((Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 0)) div ((Comput ((ProgramPart s1),s1,((4 * i) + 1))) . (dl. 1)) by A35, A49, A54, Th6
.= (Comput ((ProgramPart s2),s2,((4 * i) + 2))) . (dl. 0) by A30, A49, A51, A46, A48, Th6 ;
A60: ((4 * i) + 3) + 1 = (4 * i) + (3 + 1) ;
A61: (Comput ((ProgramPart s1),s1,((4 * i) + 3))) . (dl. 0) = (Comput ((ProgramPart s1),s1,((4 * i) + 2))) . (dl. 2) by A35, A50, A57, Th7
.= (Comput ((ProgramPart s2),s2,((4 * i) + 3))) . (dl. 0) by A30, A50, A52, A55, Th7 ;
A62: (Comput ((ProgramPart s1),s1,((4 * i) + 3))) . (dl. 1) = (Comput ((ProgramPart s1),s1,((4 * i) + 2))) . (dl. 1) by A35, A50, A57, Th7
.= (Comput ((ProgramPart s2),s2,((4 * i) + 3))) . (dl. 1) by A30, A50, A52, A56, Th7 ;
( (Comput ((ProgramPart s1),s1,((4 * i) + 3))) . (dl. 1) <= 0 or (Comput ((ProgramPart s1),s1,((4 * i) + 3))) . (dl. 1) > 0 ) ;
then ( ( IC (Comput ((ProgramPart s1),s1,((4 * i) + 4))) = 4 & IC (Comput ((ProgramPart s2),s2,((4 * i) + 4))) = 4 ) or ( IC (Comput ((ProgramPart s1),s1,((4 * i) + 4))) = 0 & IC (Comput ((ProgramPart s2),s2,((4 * i) + 4))) = 0 ) ) by A35, A30, A60, A58, A53, A62, Th8;
hence (Comput ((ProgramPart s1),s1,((4 * i) + j))) . (IC SCM) = (Comput ((ProgramPart s2),s2,((4 * i) + j))) . (IC SCM) by A43, A54, A51, A57, A52, A58, A53; :: thesis: ( (Comput ((ProgramPart s1),s1,((4 * i) + j))) . (dl. 0) = (Comput ((ProgramPart s2),s2,((4 * i) + j))) . (dl. 0) & (Comput ((ProgramPart s1),s1,((4 * i) + j))) . (dl. 1) = (Comput ((ProgramPart s2),s2,((4 * i) + j))) . (dl. 1) )
(Comput ((ProgramPart s1),s1,((4 * i) + 4))) . (dl. 0) = (Comput ((ProgramPart s1),s1,((4 * i) + 3))) . (dl. 0) by A35, A60, A58, Th8
.= (Comput ((ProgramPart s2),s2,((4 * i) + 4))) . (dl. 0) by A30, A60, A53, A61, Th8 ;
hence (Comput ((ProgramPart s1),s1,((4 * i) + j))) . (dl. 0) = (Comput ((ProgramPart s2),s2,((4 * i) + j))) . (dl. 0) by A43, A46, A59, A61; :: thesis: (Comput ((ProgramPart s1),s1,((4 * i) + j))) . (dl. 1) = (Comput ((ProgramPart s2),s2,((4 * i) + j))) . (dl. 1)
(Comput ((ProgramPart s1),s1,((4 * i) + 4))) . (dl. 1) = (Comput ((ProgramPart s1),s1,((4 * i) + 3))) . (dl. 1) by A35, A60, A58, Th8
.= (Comput ((ProgramPart s2),s2,((4 * i) + 4))) . (dl. 1) by A30, A60, A53, A62, Th8 ;
hence (Comput ((ProgramPart s1),s1,((4 * i) + j))) . (dl. 1) = (Comput ((ProgramPart s2),s2,((4 * i) + j))) . (dl. 1) by A43, A48, A56, A62; :: thesis: verum
end;
suppose A63: IC (Comput ((ProgramPart s2),s2,(4 * i))) = 4 ; :: thesis: S2[(4 * i) + j]
then ProgramPart s1 halts_at IC (Comput ((ProgramPart s1),s1,(4 * i))) by A35, A39, Lm3;
then A64: Comput ((ProgramPart s1),s1,((4 * i) + j)) = Comput ((ProgramPart s1),s1,(4 * i)) by EXTPRO_1:20, NAT_1:11;
ProgramPart s2 halts_at IC (Comput ((ProgramPart s2),s2,(4 * i))) by A30, A63, Lm3;
hence S2[(4 * i) + j] by A39, A40, A41, A64, EXTPRO_1:20, NAT_1:11; :: thesis: verum
end;
end;
end;
(Comput ((ProgramPart s1),s1,0)) . (IC SCM) = IC s1 by EXTPRO_1:3
.= 0 by A33, COMPOS_1:def 16
.= IC s2 by A37, COMPOS_1:def 16
.= (Comput ((ProgramPart s2),s2,0)) . (IC SCM) by EXTPRO_1:3 ;
then A65: S2[ 0 ] by A11, A27, A29, A32;
A66: 4 > 0 ;
U1: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
U2: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,k)) by AMI_1:123;
S2[k] from NAT_D:sch 2(A65, A66, A38);
then A67: (Comput ((ProgramPart s1),s1,k)) | {(IC SCM),(dl. 0),(dl. 1)} = (Comput ((ProgramPart s2),s2,k)) | {(IC SCM),(dl. 0),(dl. 1)} by A34, GRFUNC_1:92;
5 c= NAT by ORDINAL1:def 2;
then XX: ( (Comput ((ProgramPart s1),s1,k)) | 5 = (ProgramPart s1) | 5 & (Comput ((ProgramPart s2),s2,k)) | 5 = (ProgramPart s2) | 5 ) by U1, U2, RELAT_1:103;
dom (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) = ({(IC SCM)} \/ 5) \/ {(dl. 0),(dl. 1)} by A8, A14, FUNCT_4:def 1
.= ({(IC SCM)} \/ {(dl. 0),(dl. 1)}) \/ 5 by XBOOLE_1:4
.= {(IC SCM),(dl. 0),(dl. 1)} \/ 5 by ENUMSET1:42 ;
hence (Comput ((ProgramPart s1),s1,k)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) = (Comput ((ProgramPart s2),s2,k)) | (proj1 (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) by A36, A67, XX, RELAT_1:185; :: thesis: verum
end;
take d ; :: thesis: ( x = d & ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is Autonomy of ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) & Euclide-Function . d c= Result ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) )
thus x = d ; :: thesis: ( ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is Autonomy of ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) & Euclide-Function . d c= Result ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) )
A68: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is halting
proof
reconsider i19 = i1, i29 = i2 as Element of NAT by A4, A5, INT_1:16;
let t be State of SCM; :: according to EXTPRO_1:def 10 :: thesis: ( not ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t or ProgramPart t halts_on t )
set t9 = Comput ((ProgramPart t),t,4);
assume A69: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t ; :: thesis: ProgramPart t halts_on t
then B70: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= ProgramPart t by RELAT_1:105;
then A70: Euclide-Algorithm c= ProgramPart t by A25, XBOOLE_1:1;
A71: t . (dl. 1) = i2 by A11, A69;
A72: ( t is 0 -started & t . (dl. 0) = i1 ) by A23, A11, A69, COMPOS_1:8;
per cases ( i1 > i2 or i1 = i2 or i1 < i2 ) by XXREAL_0:1;
suppose A73: i1 = i2 ; :: thesis: ProgramPart t halts_on t
A74: i1 mod i2 = i19 mod i29
.= 0 by A73, NAT_D:25 ;
A75: Comput ((ProgramPart t),t,4) = Comput ((ProgramPart t),t,(4 * (0 + 1))) ;
t = Comput ((ProgramPart t),t,(4 * 0)) by EXTPRO_1:3;
then (Comput ((ProgramPart t),t,4)) . (dl. 1) = (t . (dl. 0)) mod (t . (dl. 1)) by A4, A5, A70, A72, A71, A75, Lm5;
then IC (Comput ((ProgramPart t),t,4)) = 4 by A4, A5, A70, A72, A71, A74, A75, Lm4;
then ProgramPart t halts_at IC (Comput ((ProgramPart t),t,4)) by A70, Lm3;
hence ProgramPart t halts_on t by EXTPRO_1:16; :: thesis: verum
end;
suppose A76: i1 < i2 ; :: thesis: ProgramPart t halts_on t
A77: Comput ((ProgramPart t),t,4) = Comput ((ProgramPart t),t,(4 * (0 + 1))) ;
A78: Euclide-Algorithm c= ProgramPart t by B70, A25, XBOOLE_1:1;
A79: t = Comput ((ProgramPart t),t,(4 * 0)) by EXTPRO_1:3;
i1 mod i2 = i19 mod i29
.= i19 by A76, NAT_D:24 ;
then A80: (Comput ((ProgramPart t),t,4)) . (dl. 1) = i1 by A4, A5, A70, A72, A71, A79, A77, Lm5;
then IC (Comput ((ProgramPart t),t,4)) = 0 by A4, A5, A70, A72, A71, A77, Lm4;
then A81: Comput ((ProgramPart t),t,4) is 0 -started by COMPOS_1:def 20;
(Comput ((ProgramPart t),t,4)) . (dl. 0) = i2 by A4, A5, A70, A72, A71, A79, A77, Lm5;
then consider k0 being Element of NAT such that
A82: ProgramPart t halts_at IC (Comput ((ProgramPart t),(Comput ((ProgramPart t),t,4)),k0)) by A4, A76, A80, A81, A78, Lm6;
ProgramPart t halts_at IC (Comput ((ProgramPart t),t,(k0 + 4))) by A82, EXTPRO_1:5;
hence ProgramPart t halts_on t by EXTPRO_1:16; :: thesis: verum
end;
end;
end;
( dl. 0 <> IC SCM & dl. 1 <> IC SCM ) by AMI_3:57;
then ( not dl. 0 in {(IC SCM)} & not dl. 1 in {(IC SCM)} ) by TARSKI:def 1;
then K: dom d misses {(IC SCM)} by A8, ZFMISC_1:57;
xx: now
assume dom d meets NAT ; :: thesis: contradiction
then consider x being set such that
W1: x in dom d and
W2: x in NAT by XBOOLE_0:3;
( x = dl. 0 or x = dl. 1 ) by W1, A8, TARSKI:def 2;
hence contradiction by W2, AMI_3:56; :: thesis: verum
end;
then dom d misses {(IC SCM)} \/ NAT by K, XBOOLE_1:70;
then d is data-only by COMPOS_1:def 23;
then NN: dom d misses NAT by COMPOS_1:40;
then KK: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) = ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) by FUNCT_4:76;
dom (ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)) c= NAT by RELAT_1:def 18;
then XX: dom d misses dom (ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)) by NN, XBOOLE_1:63;
ProgramPart (Start-At (0,SCM)) = {} by COMPOS_1:27;
then ProgramPart Euclide-Algorithm = (ProgramPart (Start-At (0,SCM))) +* (ProgramPart Euclide-Algorithm) by FUNCT_4:21
.= ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) by FUNCT_4:75 ;
then SS: ProgramPart (d +* Euclide-Algorithm) = (ProgramPart d) +* (ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)) by FUNCT_4:75
.= ProgramPart (d +* ((Start-At (0,SCM)) +* Euclide-Algorithm)) by FUNCT_4:75
.= ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) by A15, FUNCT_4:36 ;
(((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) +* (ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)) = ((Start-At (0,SCM)) +* Euclide-Algorithm) +* (d +* (ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm))) by FUNCT_4:15
.= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)) +* d) by XX, FUNCT_4:36
.= (((Start-At (0,SCM)) +* Euclide-Algorithm) +* (ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm))) +* d by FUNCT_4:15
.= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by FUNCT_4:80 ;
hence ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is Autonomy of ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) by A26, A68, EXTPRO_1:def 11; :: thesis: Euclide-Function . d c= Result ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* d))
then A83: Result ((ProgramPart (d +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) = (Result ((ProgramPart t),t)) | (dom (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) by A7, EXTPRO_1:def 12, KK, SS;
dl. 0 in the carrier of SCM ;
then A84: dl. 0 in dom (Result ((ProgramPart t),t)) by PARTFUN1:def 4;
Euclide-Algorithm c= (Start-At (0,SCM)) +* Euclide-Algorithm by FUNCT_4:26;
then A85: Euclide-Algorithm c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by A19, XBOOLE_1:1;
A86: d . (dl. 0) = i1 by A6, AMI_3:52, FUNCT_4:66;
A87: d . (dl. 1) = i2 by A6, FUNCT_4:66;
A88: d c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by FUNCT_4:26;
then A89: dom d c= dom (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) by RELAT_1:25;
A90: d c= t by A7, A88, XBOOLE_1:1;
A91: dom d = {(dl. 0),(dl. 1)} by A6, FUNCT_4:65;
then dl. 1 in dom d by TARSKI:def 2;
then A92: t . (dl. 1) = i2 by A90, A87, GRFUNC_1:8;
XX0: Euclide-Algorithm c= t by A7, A85, XBOOLE_1:1;
dl. 0 in dom d by A91, TARSKI:def 2;
then t . (dl. 0) = i1 by A90, A86, GRFUNC_1:8;
then A93: (Result ((ProgramPart t),t)) . (dl. 0) = i1 gcd i2 by A4, A5, A24, A92, Th10, XX0, RELAT_1:210;
x2: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) = ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) by FUNCT_4:76, xx;
x3: dom ((dl. 0) .--> (i1 gcd i2)) = {(dl. 0)} by FUNCOP_1:19;
dom ((dl. 0) .--> (i1 gcd i2)) c= dom d by A91, x3, ZFMISC_1:12;
then A94: dom ((dl. 0) .--> (i1 gcd i2)) c= dom (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) by A89, XBOOLE_1:1;
Euclide-Function . d = (dl. 0) .--> (i1 gcd i2) by A4, A5, A6, Th12;
hence Euclide-Function . d c= Result ((ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm)),(((Start-At (0,SCM)) +* Euclide-Algorithm) +* d)) by A84, A93, A94, A83, x2, FUNCT_4:90, RELAT_1:186, SS; :: thesis: verum