let e1, e2 be NAT * -defined to-naturals homogeneous Function; for i being Nat
for p, q being FinSequence of NAT holds primrec (e1,e2,i,p) tolerates primrec (e1,e2,i,q)
let i be Nat; 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,p2)then
(
primrec (
e1,
e2,
i,
p1)
= {} or
primrec (
e1,
e2,
i,
p2)
= {} )
by Th49;
hence
primrec (
e1,
e2,
i,
p1)
tolerates primrec (
e1,
e2,
i,
p2)
;
verum end; suppose A1:
(
i in dom p1 &
i in dom p2 )
;
primrec (e1,e2,i,p1) tolerates primrec (e1,e2,i,p2)reconsider m =
p1 /. i,
n =
p2 /. i as
Element of
NAT ;
consider F2 being
sequence of
(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
Nat holds
S1[
m,
F2 . m,
F2 . (m + 1),
p2,
i,
e2]
by Def10;
consider F1 being
sequence of
(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
Nat holds
S1[
m,
F1 . m,
F1 . (m + 1),
p1,
i,
e2]
by Def10;
defpred S2[
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 for m being Nat st S2[m] holds
S2[m + 1]let m be
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)))}
;
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; end; A15:
now ( p1 +* (i,0) = p2 +* (i,0) implies for m being Nat holds S3[m] )defpred S3[
Nat]
means F1 . $1
= F2 . $1;
assume A16:
p1 +* (
i,
0)
= p2 +* (
i,
0)
;
for m being Nat holds S3[m]A17:
S3[
0 ]
A18:
now for m being Nat st S3[m] holds
S3[m + 1]let m be
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, Th2;
hence
S3[
m + 1]
by A1, A19, A20, A21, Th2;
verum end; thus
for
m being
Nat holds
S3[
m]
from NAT_1:sch 2(A17, A18); verum end; A22:
S2[
0 ]
A24:
for
m being
Nat holds
S2[
m]
from NAT_1:sch 2(A22, A10);
A25:
for
m,
n being
Nat holds
F1 . m c= F1 . (m + n)
proof
let m be
Nat;
for n being Nat holds F1 . m c= F1 . (m + n)
defpred S3[
Nat]
means F1 . m c= F1 . (m + $1);
A26:
now for n being Nat st S3[n] holds
S3[n + 1]let n be
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
object ;
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
object 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:31;
A35:
x = p1 +* (
i,
((m + n) + 1))
by A31, TARSKI:def 1;
n1 = (p1 +* (i,n1)) . i
by A1, FUNCT_7:31;
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:32;
hence
x in F1 . ((m + n) + 1)
by A28;
verum end; end;
end; hence
S3[
n + 1]
by A27, XBOOLE_1:1;
verum end;
A36:
S3[
0 ]
;
thus
for
n being
Nat holds
S3[
n]
from NAT_1:sch 2(A36, A26); verum
end; defpred S3[
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 for m being Nat st S3[m] holds
S3[m + 1]let m be
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)))}
;
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; end; A42:
S3[
0 ]
A44:
for
m being
Nat holds
S3[
m]
from NAT_1:sch 2(A42, A37);
A45:
for
m,
n being
Nat holds
F2 . m c= F2 . (m + n)
proof
let m be
Nat;
for n being Nat holds F2 . m c= F2 . (m + n)
defpred S4[
Nat]
means F2 . m c= F2 . (m + $1);
A46:
now for n being Nat st S4[n] holds
S4[n + 1]let n be
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
object ;
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
object 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:31;
A55:
x = p2 +* (
i,
((m + n) + 1))
by A51, TARSKI:def 1;
n2 = (p2 +* (i,n2)) . i
by A1, FUNCT_7:31;
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:32;
hence
x in F2 . ((m + n) + 1)
by A48;
verum end; end;
end; hence
S4[
n + 1]
by A47, XBOOLE_1:1;
verum end;
A56:
S4[
0 ]
;
thus
for
n being
Nat holds
S4[
n]
from NAT_1:sch 2(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,p2)then consider k being
Nat such that A61:
n = m + k
by NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
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,p2)hence
primrec (
e1,
e2,
i,
p1)
tolerates primrec (
e1,
e2,
i,
p2)
by A6, A2, A25, A62, PARTFUN1:58;
verum end; suppose
(dom F1n) /\ (dom F2n) = {}
;
primrec (e1,e2,i,p1) tolerates primrec (e1,e2,i,p2)then
dom F1n misses dom F2n
by XBOOLE_0:def 7;
then
F1n tolerates F2n
by PARTFUN1:56;
hence
primrec (
e1,
e2,
i,
p1)
tolerates primrec (
e1,
e2,
i,
p2)
by A6, A2, A25, A62, PARTFUN1:58;
verum end; end;
end; end; suppose
m >= n
;
primrec (e1,e2,i,p1) tolerates primrec (e1,e2,i,p2)then consider k being
Nat such that A63:
m = n + k
by NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
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,p2)hence
primrec (
e1,
e2,
i,
p1)
tolerates primrec (
e1,
e2,
i,
p2)
by A6, A2, A45, A64, PARTFUN1:58;
verum end; suppose
(dom F1m) /\ (dom F2m) = {}
;
primrec (e1,e2,i,p1) tolerates primrec (e1,e2,i,p2)then
dom F1m misses dom F2m
by XBOOLE_0:def 7;
then
F1m tolerates F2m
by PARTFUN1:56;
hence
primrec (
e1,
e2,
i,
p1)
tolerates primrec (
e1,
e2,
i,
p2)
by A6, A2, A45, A64, PARTFUN1:58;
verum end; end;
end; end; end;
end; end; end;