let e1, e2 be NAT * -defined to-naturals homogeneous Function; :: thesis: 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; :: 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,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) ; :: thesis: verum
end;
suppose A1: ( i in dom p1 & i in dom p2 ) ; :: thesis: 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 :: thesis: for m being Nat st S2[m] holds
S2[m + 1]
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A11: S2[m] ; :: thesis: S2[m + 1]
thus S2[m + 1] :: thesis: verum
proof
set p1c = (p1 +* (i,m)) ^ <*((F1 . m) . (p1 +* (i,m)))*>;
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 A12: x in dom (F1 . (m + 1)) ; :: thesis: 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 ) ; :: 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 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 ) :: thesis: verum
proof
per cases ( x in dom (F1 . m) or x = p1 +* (i,(m + 1)) ) by A14, TARSKI:def 1;
suppose x in dom (F1 . m) ; :: thesis: ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m + 1 )
then ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m ) by A11;
hence ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m + 1 ) by A13, XXREAL_0:2; :: thesis: verum
end;
suppose x = p1 +* (i,(m + 1)) ; :: thesis: ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m + 1 )
hence ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m + 1 ) ; :: thesis: verum
end;
end;
end;
end;
suppose ( 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 ) ; :: thesis: ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m + 1 )
then F1 . (m + 1) = F1 . m by A9;
then ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m ) by A11, A12;
hence ex n being Element of NAT st
( x = p1 +* (i,n) & n <= m + 1 ) by A13, XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
A15: now :: thesis: ( 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) ; :: thesis: for m being Nat holds S3[m]
A17: S3[ 0 ]
proof
per cases ( ( i in dom p1 & Del (p1,i) in dom e1 ) or not i in dom p1 or not Del (p1,i) in dom e1 ) ;
suppose ( i in dom p1 & Del (p1,i) in dom e1 ) ; :: thesis: S3[ 0 ]
hence S3[ 0 ] by A1, A7, A3, A16, Th4; :: thesis: verum
end;
suppose ( not i in dom p1 or not Del (p1,i) in dom e1 ) ; :: thesis: S3[ 0 ]
hence S3[ 0 ] by A1, A8, A4, A16, Th4; :: thesis: verum
end;
end;
end;
A18: now :: thesis: for m being Nat st S3[m] holds
S3[m + 1]
let m be Nat; :: thesis: ( S3[m] implies S3[m + 1] )
assume A19: S3[m] ; :: thesis: 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; :: thesis: verum
end;
thus for m being Nat holds S3[m] from NAT_1:sch 2(A17, A18); :: thesis: verum
end;
A22: S2[ 0 ]
proof
let x be set ; :: thesis: ( x in dom (F1 . 0) implies ex n being Element of NAT st
( x = p1 +* (i,n) & n <= 0 ) )
assume A23: x in dom (F1 . 0) ; :: thesis: ex n being Element of NAT st
( x = p1 +* (i,n) & n <= 0 )
dom (F1 . 0) = {(p1 +* (i,0))} by A7, A8, A23;
then x = p1 +* (i,0) by A23, TARSKI:def 1;
hence ex n being Element of NAT st
( x = p1 +* (i,n) & n <= 0 ) ; :: thesis: verum
end;
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; :: thesis: for n being Nat holds F1 . m c= F1 . (m + n)
defpred S3[ Nat] means F1 . m c= F1 . (m + $1);
A26: now :: thesis: for n being Nat st S3[n] holds
S3[n + 1]
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A27: S3[n] ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in F1 . (m + n) or x in F1 . ((m + n) + 1) )
assume A28: x in F1 . (m + n) ; :: thesis: 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 ) ; :: thesis: 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))))*>))) ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
suppose ( 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 ) ; :: thesis: x in F1 . ((m + n) + 1)
hence x in F1 . ((m + n) + 1) by A9, A28; :: thesis: verum
end;
end;
end;
hence S3[n + 1] by A27, XBOOLE_1:1; :: thesis: verum
end;
A36: S3[ 0 ] ;
thus for n being Nat holds S3[n] from NAT_1:sch 2(A36, A26); :: thesis: 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 :: thesis: for m being Nat st S3[m] holds
S3[m + 1]
let m be Nat; :: thesis: ( S3[m] implies S3[m + 1] )
assume A38: S3[m] ; :: thesis: S3[m + 1]
thus S3[m + 1] :: thesis: verum
proof
set p2c = (p2 +* (i,m)) ^ <*((F2 . m) . (p2 +* (i,m)))*>;
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 A39: x in dom (F2 . (m + 1)) ; :: thesis: 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 ) ; :: 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 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 ) :: thesis: verum
proof
per cases ( x in dom (F2 . m) or x = p2 +* (i,(m + 1)) ) by A41, TARSKI:def 1;
suppose x in dom (F2 . m) ; :: thesis: ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m + 1 )
then ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m ) by A38;
hence ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m + 1 ) by A40, XXREAL_0:2; :: thesis: verum
end;
suppose x = p2 +* (i,(m + 1)) ; :: thesis: ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m + 1 )
hence ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m + 1 ) ; :: thesis: verum
end;
end;
end;
end;
suppose ( 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 ) ; :: thesis: ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m + 1 )
then F2 . (m + 1) = F2 . m by A5;
then ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m ) by A38, A39;
hence ex n being Element of NAT st
( x = p2 +* (i,n) & n <= m + 1 ) by A40, XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
A42: S3[ 0 ]
proof
let x be set ; :: thesis: ( x in dom (F2 . 0) implies ex n being Element of NAT st
( x = p2 +* (i,n) & n <= 0 ) )
assume A43: x in dom (F2 . 0) ; :: thesis: ex n being Element of NAT st
( x = p2 +* (i,n) & n <= 0 )
dom (F2 . 0) = {(p2 +* (i,0))} by A3, A4, A43;
then x = p2 +* (i,0) by A43, TARSKI:def 1;
hence ex n being Element of NAT st
( x = p2 +* (i,n) & n <= 0 ) ; :: thesis: verum
end;
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; :: thesis: for n being Nat holds F2 . m c= F2 . (m + n)
defpred S4[ Nat] means F2 . m c= F2 . (m + $1);
A46: now :: thesis: for n being Nat st S4[n] holds
S4[n + 1]
let n be Nat; :: thesis: ( S4[n] implies S4[n + 1] )
assume A47: S4[n] ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in F2 . (m + n) or x in F2 . ((m + n) + 1) )
assume A48: x in F2 . (m + n) ; :: thesis: 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 ) ; :: thesis: 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))))*>))) ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
suppose ( 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 ) ; :: thesis: x in F2 . ((m + n) + 1)
hence x in F2 . ((m + n) + 1) by A5, A48; :: thesis: verum
end;
end;
end;
hence S4[n + 1] by A47, XBOOLE_1:1; :: thesis: verum
end;
A56: S4[ 0 ] ;
thus for n being Nat holds S4[n] from NAT_1:sch 2(A56, A46); :: thesis: verum
end;
reconsider F1m = F1 . m, F1n = F1 . n, F2m = F2 . m, F2n = F2 . n as Element of HFuncs NAT ;
A57: now :: thesis: ( p1 +* (i,0) <> p2 +* (i,0) implies for m being Element of NAT holds not (dom (F1 . m)) /\ (dom (F2 . m)) <> {} )
assume A58: p1 +* (i,0) <> p2 +* (i,0) ; :: thesis: for m being Element of NAT holds not (dom (F1 . m)) /\ (dom (F2 . m)) <> {}
let m be Element of NAT ; :: thesis: not (dom (F1 . m)) /\ (dom (F2 . m)) <> {}
assume (dom (F1 . m)) /\ (dom (F2 . m)) <> {} ; :: thesis: contradiction
then consider x being object such that
A59: x in (dom (F1 . m)) /\ (dom (F2 . m)) by XBOOLE_0:def 1;
x in dom (F2 . m) by A59, XBOOLE_0:def 4;
then A60: ex n2 being Element of NAT st
( x = p2 +* (i,n2) & n2 <= m ) by A44;
x in dom (F1 . m) by A59, XBOOLE_0:def 4;
then ex n1 being Element of NAT st
( x = p1 +* (i,n1) & n1 <= m ) by A24;
hence contradiction by A58, A60, Th2; :: thesis: verum
end;
thus primrec (e1,e2,i,p1) tolerates primrec (e1,e2,i,p2) :: thesis: verum
proof
per cases ( m <= n or m >= n ) ;
suppose m <= n ; :: thesis: 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) :: thesis: verum
proof
per cases ( F1n = F2n or (dom F1n) /\ (dom F2n) = {} ) by A15, A57;
suppose F1n = F2n ; :: thesis: 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; :: thesis: verum
end;
suppose (dom F1n) /\ (dom F2n) = {} ; :: thesis: 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; :: thesis: verum
end;
end;
end;
end;
suppose m >= n ; :: thesis: 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) :: thesis: verum
proof
per cases ( F1m = F2m or (dom F1m) /\ (dom F2m) = {} ) by A15, A57;
suppose F1m = F2m ; :: thesis: 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; :: thesis: verum
end;
suppose (dom F1m) /\ (dom F2m) = {} ; :: thesis: 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; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;