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