let i be Element of NAT ; for e1, e2 being NAT * -defined to-naturals homogeneous Function
for p, q being FinSequence of NAT holds primrec e1,e2,i,p tolerates primrec e1,e2,i,q
let e1, e2 be NAT * -defined to-naturals homogeneous Function; for p, q being FinSequence of NAT holds primrec e1,e2,i,p tolerates primrec e1,e2,i,q
set f1 = e1;
set f2 = e2;
let p1, p2 be FinSequence of NAT ; primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2
per cases
( not i in dom p1 or not i in dom p2 or ( i in dom p1 & i in dom p2 ) )
;
suppose
( not
i in dom p1 or not
i in dom p2 )
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2then
(
primrec e1,
e2,
i,
p1 = {} or
primrec e1,
e2,
i,
p2 = {} )
by Th54;
hence
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
by PARTFUN1:141;
verum end; suppose A1:
(
i in dom p1 &
i in dom p2 )
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2reconsider m =
p1 /. i,
n =
p2 /. i as
Element of
NAT ;
consider F2 being
Function of
NAT ,
(HFuncs NAT ) such that A2:
primrec e1,
e2,
i,
p2 = F2 . (p2 /. i)
and A3:
(
i in dom p2 &
Del p2,
i in dom e1 implies
F2 . 0 = (p2 +* i,0 ) .--> (e1 . (Del p2,i)) )
and A4:
( ( not
i in dom p2 or not
Del p2,
i in dom e1 ) implies
F2 . 0 = {} )
and A5:
for
m being
Element of
NAT holds
S1[
m,
F2 . m,
F2 . (m + 1),
p2,
i,
e2]
by Def13;
consider F1 being
Function of
NAT ,
(HFuncs NAT ) such that A6:
primrec e1,
e2,
i,
p1 = F1 . (p1 /. i)
and A7:
(
i in dom p1 &
Del p1,
i in dom e1 implies
F1 . 0 = (p1 +* i,0 ) .--> (e1 . (Del p1,i)) )
and A8:
( ( not
i in dom p1 or not
Del p1,
i in dom e1 ) implies
F1 . 0 = {} )
and A9:
for
m being
Element of
NAT holds
S1[
m,
F1 . m,
F1 . (m + 1),
p1,
i,
e2]
by Def13;
defpred S2[
Element of
NAT ]
means for
x being
set st
x in dom (F1 . $1) holds
ex
n being
Element of
NAT st
(
x = p1 +* i,
n &
n <= $1 );
A10:
now let m be
Element of
NAT ;
( S2[m] implies S2[m + 1] )assume A11:
S2[
m]
;
S2[m + 1]thus
S2[
m + 1]
verumproof
set p1c =
(p1 +* i,m) ^ <*((F1 . m) . (p1 +* i,m))*>;
let x be
set ;
( x in dom (F1 . (m + 1)) implies ex n being Element of NAT st
( x = p1 +* i,n & n <= m + 1 ) )
assume A12:
x in dom (F1 . (m + 1))
;
ex n being Element of NAT st
( x = p1 +* i,n & n <= m + 1 )
A13:
m <= m + 1
by NAT_1:11;
per cases
( ( i in dom p1 & p1 +* i,m in dom (F1 . m) & (p1 +* i,m) ^ <*((F1 . m) . (p1 +* i,m))*> in dom e2 ) or not i in dom p1 or not p1 +* i,m in dom (F1 . m) or not (p1 +* i,m) ^ <*((F1 . m) . (p1 +* i,m))*> in dom e2 )
;
suppose
(
i in dom p1 &
p1 +* i,
m in dom (F1 . m) &
(p1 +* i,m) ^ <*((F1 . m) . (p1 +* i,m))*> in dom e2 )
;
ex n being Element of NAT st
( x = p1 +* i,n & n <= m + 1 )then
F1 . (m + 1) = (F1 . m) +* ((p1 +* i,(m + 1)) .--> (e2 . ((p1 +* i,m) ^ <*((F1 . m) . (p1 +* i,m))*>)))
by A9;
then dom (F1 . (m + 1)) =
(dom (F1 . m)) \/ (dom ((p1 +* i,(m + 1)) .--> (e2 . ((p1 +* i,m) ^ <*((F1 . m) . (p1 +* i,m))*>))))
by FUNCT_4:def 1
.=
(dom (F1 . m)) \/ {(p1 +* i,(m + 1))}
by FUNCOP_1:19
;
then A14:
(
x in dom (F1 . m) or
x in {(p1 +* i,(m + 1))} )
by A12, XBOOLE_0:def 3;
thus
ex
n being
Element of
NAT st
(
x = p1 +* i,
n &
n <= m + 1 )
verum end;
end; end; A15:
now defpred S3[
Element of
NAT ]
means F1 . $1
= F2 . $1;
assume A16:
p1 +* i,
0 = p2 +* i,
0
;
for m being Element of NAT holds S3[m]A17:
S3[
0 ]
A18:
now let m be
Element of
NAT ;
( S3[m] implies S3[m + 1] )assume A19:
S3[
m]
;
S3[m + 1]A20:
S1[
m,
F1 . m,
F1 . (m + 1),
p1,
i,
e2]
by A9;
A21:
S1[
m,
F2 . m,
F2 . (m + 1),
p2,
i,
e2]
by A5;
p1 +* i,
m = p2 +* i,
m
by A16, Th5;
hence
S3[
m + 1]
by A1, A19, A20, A21, Th5;
verum end; thus
for
m being
Element of
NAT holds
S3[
m]
from NAT_1:sch 1(A17, A18); verum end; A22:
S2[
0 ]
A24:
for
m being
Element of
NAT holds
S2[
m]
from NAT_1:sch 1(A22, A10);
A25:
for
m,
n being
Element of
NAT holds
F1 . m c= F1 . (m + n)
proof
let m be
Element of
NAT ;
for n being Element of NAT holds F1 . m c= F1 . (m + n)
defpred S3[
Element of
NAT ]
means F1 . m c= F1 . (m + $1);
A26:
now let n be
Element of
NAT ;
( S3[n] implies S3[n + 1] )assume A27:
S3[
n]
;
S3[n + 1]set k =
m + n;
F1 . (m + n) c= F1 . ((m + n) + 1)
proof
set p1c =
(p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*>;
let x be
set ;
TARSKI:def 3 ( not x in F1 . (m + n) or x in F1 . ((m + n) + 1) )
assume A28:
x in F1 . (m + n)
;
x in F1 . ((m + n) + 1)
per cases
( ( i in dom p1 & p1 +* i,(m + n) in dom (F1 . (m + n)) & (p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*> in dom e2 ) or not i in dom p1 or not p1 +* i,(m + n) in dom (F1 . (m + n)) or not (p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*> in dom e2 )
;
suppose A29:
(
i in dom p1 &
p1 +* i,
(m + n) in dom (F1 . (m + n)) &
(p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*> in dom e2 )
;
x in F1 . ((m + n) + 1)A30:
dom (F1 . (m + n)) misses dom ((p1 +* i,((m + n) + 1)) .--> (e2 . ((p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*>)))
proof
assume
not
dom (F1 . (m + n)) misses dom ((p1 +* i,((m + n) + 1)) .--> (e2 . ((p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*>)))
;
contradiction
then consider x being
set such that A31:
x in (dom (F1 . (m + n))) /\ (dom ({(p1 +* i,((m + n) + 1))} --> (e2 . ((p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*>))))
by XBOOLE_0:4;
x in dom (F1 . (m + n))
by A31, XBOOLE_0:def 4;
then consider n1 being
Element of
NAT such that A32:
x = p1 +* i,
n1
and A33:
n1 <= m + n
by A24;
A34:
(m + n) + 1
= (p1 +* i,((m + n) + 1)) . i
by A1, FUNCT_7:33;
A35:
x = p1 +* i,
((m + n) + 1)
by A31, TARSKI:def 1;
n1 = (p1 +* i,n1) . i
by A1, FUNCT_7:33;
hence
contradiction
by A35, A32, A33, A34, NAT_1:13;
verum
end;
F1 . ((m + n) + 1) = (F1 . (m + n)) +* ((p1 +* i,((m + n) + 1)) .--> (e2 . ((p1 +* i,(m + n)) ^ <*((F1 . (m + n)) . (p1 +* i,(m + n)))*>)))
by A9, A29;
then
F1 . (m + n) c= F1 . ((m + n) + 1)
by A30, FUNCT_4:33;
hence
x in F1 . ((m + n) + 1)
by A28;
verum end;
end; hence
S3[
n + 1]
by A27, XBOOLE_1:1;
verum end;
A36:
S3[
0 ]
;
thus
for
n being
Element of
NAT holds
S3[
n]
from NAT_1:sch 1(A36, A26); verum
end; defpred S3[
Element of
NAT ]
means for
x being
set st
x in dom (F2 . $1) holds
ex
n being
Element of
NAT st
(
x = p2 +* i,
n &
n <= $1 );
A37:
now let m be
Element of
NAT ;
( S3[m] implies S3[m + 1] )assume A38:
S3[
m]
;
S3[m + 1]thus
S3[
m + 1]
verumproof
set p2c =
(p2 +* i,m) ^ <*((F2 . m) . (p2 +* i,m))*>;
let x be
set ;
( x in dom (F2 . (m + 1)) implies ex n being Element of NAT st
( x = p2 +* i,n & n <= m + 1 ) )
assume A39:
x in dom (F2 . (m + 1))
;
ex n being Element of NAT st
( x = p2 +* i,n & n <= m + 1 )
A40:
m <= m + 1
by NAT_1:11;
per cases
( ( i in dom p2 & p2 +* i,m in dom (F2 . m) & (p2 +* i,m) ^ <*((F2 . m) . (p2 +* i,m))*> in dom e2 ) or not i in dom p2 or not p2 +* i,m in dom (F2 . m) or not (p2 +* i,m) ^ <*((F2 . m) . (p2 +* i,m))*> in dom e2 )
;
suppose
(
i in dom p2 &
p2 +* i,
m in dom (F2 . m) &
(p2 +* i,m) ^ <*((F2 . m) . (p2 +* i,m))*> in dom e2 )
;
ex n being Element of NAT st
( x = p2 +* i,n & n <= m + 1 )then
F2 . (m + 1) = (F2 . m) +* ((p2 +* i,(m + 1)) .--> (e2 . ((p2 +* i,m) ^ <*((F2 . m) . (p2 +* i,m))*>)))
by A5;
then dom (F2 . (m + 1)) =
(dom (F2 . m)) \/ (dom ((p2 +* i,(m + 1)) .--> (e2 . ((p2 +* i,m) ^ <*((F2 . m) . (p2 +* i,m))*>))))
by FUNCT_4:def 1
.=
(dom (F2 . m)) \/ {(p2 +* i,(m + 1))}
by FUNCOP_1:19
;
then A41:
(
x in dom (F2 . m) or
x in {(p2 +* i,(m + 1))} )
by A39, XBOOLE_0:def 3;
thus
ex
n being
Element of
NAT st
(
x = p2 +* i,
n &
n <= m + 1 )
verum end;
end; end; A42:
S3[
0 ]
A44:
for
m being
Element of
NAT holds
S3[
m]
from NAT_1:sch 1(A42, A37);
A45:
for
m,
n being
Element of
NAT holds
F2 . m c= F2 . (m + n)
proof
let m be
Element of
NAT ;
for n being Element of NAT holds F2 . m c= F2 . (m + n)
defpred S4[
Element of
NAT ]
means F2 . m c= F2 . (m + $1);
A46:
now let n be
Element of
NAT ;
( S4[n] implies S4[n + 1] )assume A47:
S4[
n]
;
S4[n + 1]set k =
m + n;
F2 . (m + n) c= F2 . ((m + n) + 1)
proof
set p2c =
(p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*>;
let x be
set ;
TARSKI:def 3 ( not x in F2 . (m + n) or x in F2 . ((m + n) + 1) )
assume A48:
x in F2 . (m + n)
;
x in F2 . ((m + n) + 1)
per cases
( ( i in dom p2 & p2 +* i,(m + n) in dom (F2 . (m + n)) & (p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*> in dom e2 ) or not i in dom p2 or not p2 +* i,(m + n) in dom (F2 . (m + n)) or not (p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*> in dom e2 )
;
suppose A49:
(
i in dom p2 &
p2 +* i,
(m + n) in dom (F2 . (m + n)) &
(p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*> in dom e2 )
;
x in F2 . ((m + n) + 1)A50:
dom (F2 . (m + n)) misses dom ((p2 +* i,((m + n) + 1)) .--> (e2 . ((p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*>)))
proof
assume
not
dom (F2 . (m + n)) misses dom ((p2 +* i,((m + n) + 1)) .--> (e2 . ((p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*>)))
;
contradiction
then consider x being
set such that A51:
x in (dom (F2 . (m + n))) /\ (dom ({(p2 +* i,((m + n) + 1))} --> (e2 . ((p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*>))))
by XBOOLE_0:4;
x in dom (F2 . (m + n))
by A51, XBOOLE_0:def 4;
then consider n2 being
Element of
NAT such that A52:
x = p2 +* i,
n2
and A53:
n2 <= m + n
by A44;
A54:
(m + n) + 1
= (p2 +* i,((m + n) + 1)) . i
by A1, FUNCT_7:33;
A55:
x = p2 +* i,
((m + n) + 1)
by A51, TARSKI:def 1;
n2 = (p2 +* i,n2) . i
by A1, FUNCT_7:33;
hence
contradiction
by A55, A52, A53, A54, NAT_1:13;
verum
end;
F2 . ((m + n) + 1) = (F2 . (m + n)) +* ((p2 +* i,((m + n) + 1)) .--> (e2 . ((p2 +* i,(m + n)) ^ <*((F2 . (m + n)) . (p2 +* i,(m + n)))*>)))
by A5, A49;
then
F2 . (m + n) c= F2 . ((m + n) + 1)
by A50, FUNCT_4:33;
hence
x in F2 . ((m + n) + 1)
by A48;
verum end;
end; hence
S4[
n + 1]
by A47, XBOOLE_1:1;
verum end;
A56:
S4[
0 ]
;
thus
for
n being
Element of
NAT holds
S4[
n]
from NAT_1:sch 1(A56, A46); verum
end; reconsider F1m =
F1 . m,
F1n =
F1 . n,
F2m =
F2 . m,
F2n =
F2 . n as
Element of
HFuncs NAT ;
thus
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
verumproof
per cases
( m <= n or m >= n )
;
suppose
m <= n
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2then consider k being
Nat such that A61:
n = m + k
by NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
A62:
n = m + k
by A61;
thus
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
verumproof
per cases
( F1n = F2n or (dom F1n) /\ (dom F2n) = {} )
by A15, A57;
suppose
F1n = F2n
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2hence
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
by A6, A2, A25, A62, PARTFUN1:140;
verum end; suppose
(dom F1n) /\ (dom F2n) = {}
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2then
dom F1n misses dom F2n
by XBOOLE_0:def 7;
then
F1n tolerates F2n
by PARTFUN1:138;
hence
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
by A6, A2, A25, A62, PARTFUN1:140;
verum end;
end; end; suppose
m >= n
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2then consider k being
Nat such that A63:
m = n + k
by NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
A64:
m = n + k
by A63;
thus
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
verumproof
per cases
( F1m = F2m or (dom F1m) /\ (dom F2m) = {} )
by A15, A57;
suppose
F1m = F2m
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2hence
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
by A6, A2, A45, A64, PARTFUN1:140;
verum end; suppose
(dom F1m) /\ (dom F2m) = {}
;
primrec e1,e2,i,p1 tolerates primrec e1,e2,i,p2then
dom F1m misses dom F2m
by XBOOLE_0:def 7;
then
F1m tolerates F2m
by PARTFUN1:138;
hence
primrec e1,
e2,
i,
p1 tolerates primrec e1,
e2,
i,
p2
by A6, A2, A45, A64, PARTFUN1:140;
verum end;
end; end;
end; end;