let D be non empty set ; for f being BinominativeFunction of D
for p, r being PartialPredicate of D st <*(PP_and (r,p)),f,p*> is SFHT of D & <*(PP_and (r,(PP_inversion p))),f,p*> is SFHT of D holds
<*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D
let f be BinominativeFunction of D; for p, r being PartialPredicate of D st <*(PP_and (r,p)),f,p*> is SFHT of D & <*(PP_and (r,(PP_inversion p))),f,p*> is SFHT of D holds
<*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D
let p, r be PartialPredicate of D; ( <*(PP_and (r,p)),f,p*> is SFHT of D & <*(PP_and (r,(PP_inversion p))),f,p*> is SFHT of D implies <*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D )
set a = PP_and (r,p);
set F = PP_while (r,f);
set q = PP_and ((PP_not r),p);
set INV = PP_inversion p;
assume that
A1:
<*(PP_and (r,p)),f,p*> is SFHT of D
and
A2:
<*(PP_and (r,(PP_inversion p))),f,p*> is SFHT of D
; <*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D
A3:
dom (PP_and (r,p)) = { d where d is Element of D : ( ( d in dom r & r . d = FALSE ) or ( d in dom p & p . d = FALSE ) or ( d in dom r & r . d = TRUE & d in dom p & p . d = TRUE ) ) }
by PARTPR_1:16;
A4:
dom (PP_inversion p) = { d where d is Element of D : not d in dom p }
by PARTPR_2:def 17;
A5:
dom (PP_and (r,(PP_inversion p))) = { d where d is Element of D : ( ( d in dom r & r . d = FALSE ) or ( d in dom (PP_inversion p) & (PP_inversion p) . d = FALSE ) or ( d in dom r & r . d = TRUE & d in dom (PP_inversion p) & (PP_inversion p) . d = TRUE ) ) }
by PARTPR_1:16;
for d being Element of D st d in dom p & p . d = TRUE & d in dom (PP_while (r,f)) & (PP_while (r,f)) . d in dom (PP_and ((PP_not r),p)) holds
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE
proof
let d be
Element of
D;
( d in dom p & p . d = TRUE & d in dom (PP_while (r,f)) & (PP_while (r,f)) . d in dom (PP_and ((PP_not r),p)) implies (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE )
assume that A6:
d in dom p
and A7:
p . d = TRUE
and A8:
d in dom (PP_while (r,f))
and A9:
(PP_while (r,f)) . d in dom (PP_and ((PP_not r),p))
;
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE
consider n being
Nat such that A10:
for
i being
Nat st
i <= n - 1 holds
(
d in dom (r * (iter (f,i))) &
(r * (iter (f,i))) . d = TRUE )
and A11:
d in dom (r * (iter (f,n)))
and A12:
(r * (iter (f,n))) . d = FALSE
and A13:
(PP_while (r,f)) . d = (iter (f,n)) . d
by A8, PARTPR_2:def 15;
reconsider I =
iter (
f,
n) as
BinominativeFunction of
D by FUNCT_7:86;
A14:
d in dom I
by A11, FUNCT_1:11;
A15:
(r * I) . d = r . (I . d)
by A11, FUNCT_1:12;
per cases
( ( (PP_while (r,f)) . d in dom (PP_not r) & (PP_not r) . ((PP_while (r,f)) . d) = FALSE ) or ( (PP_while (r,f)) . d in dom (PP_not r) & (PP_not r) . ((PP_while (r,f)) . d) = TRUE & (PP_while (r,f)) . d in dom p & p . ((PP_while (r,f)) . d) = TRUE ) or ( (PP_while (r,f)) . d in dom p & p . ((PP_while (r,f)) . d) = FALSE ) )
by A9, PARTPR_1:17;
suppose that A16:
(PP_while (r,f)) . d in dom p
and A17:
p . ((PP_while (r,f)) . d) = FALSE
;
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE A18:
iter (
f,
0)
= id (field f)
by FUNCT_7:68;
A19:
(iter (f,n)) . d in dom r
by A11, FUNCT_1:11;
A20:
dom (PP_not r) = dom r
by PARTPR_1:def 2;
A21:
now ( (iter (f,0)) . d in dom p & d in dom (iter (f,0)) & p . ((iter (f,0)) . d) = TRUE )
(
0 = n or
0 <= n - 1 )
by NAT_1:3, INT_1:52;
then
(
0 = n or
d in dom (r * (iter (f,0))) )
by A10;
then
d in dom (id (field f))
by A11, A18, FUNCT_1:11;
hence
(
(iter (f,0)) . d in dom p &
d in dom (iter (f,0)) &
p . ((iter (f,0)) . d) = TRUE )
by A6, A7, A18, FUNCT_1:18;
verum end; per cases
( n = 0 or n > 0 )
by NAT_1:3;
suppose A22:
n = 0
;
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE then
d in dom (id (field f))
by A11, A18, FUNCT_1:11;
then A23:
(iter (f,0)) . d = d
by A18, FUNCT_1:18;
then
(PP_not r) . d = TRUE
by A12, A15, A19, A22, PARTPR_1:def 2;
hence
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE
by A21, A13, A19, A20, A22, A23, PARTPR_1:18;
verum end; suppose A24:
n > 0
;
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE defpred S1[
Nat]
means ( not $1
< n or not
d in dom (iter (f,$1)) or not
(iter (f,$1)) . d in dom p or (
d in dom (iter (f,$1)) &
(iter (f,$1)) . d in dom p &
p . ((iter (f,$1)) . d) = TRUE ) );
A25:
S1[
0 ]
by A21;
A26:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A27:
S1[
i]
and A28:
i + 1
< n
and A29:
d in dom (iter (f,(i + 1)))
and A30:
(iter (f,(i + 1))) . d in dom p
;
( d in dom (iter (f,(i + 1))) & (iter (f,(i + 1))) . d in dom p & p . ((iter (f,(i + 1))) . d) = TRUE )
A31:
i <= i + 1
by NAT_1:11;
set DD =
(iter (f,i)) . d;
A32:
(i + 1) - 1
<= n - 1
by A28, XREAL_1:9;
A33:
d in dom (r * (iter (f,i)))
by A10, A32;
then A34:
d in dom (iter (f,i))
by FUNCT_1:11;
iter (
f,
i) is
BinominativeFunction of
D
by FUNCT_7:86;
then reconsider DD =
(iter (f,i)) . d as
Element of
D by A34, PARTFUN1:4;
(r * (iter (f,i))) . d = TRUE
by A10, A32;
then A35:
r . DD = TRUE
by A34, FUNCT_1:13;
A36:
DD in dom r
by A33, FUNCT_1:11;
A37:
iter (
f,
(i + 1))
= f * (iter (f,i))
by FUNCT_7:71;
A38:
f . DD = (f * (iter (f,i))) . d
by A34, FUNCT_1:13;
per cases
( not DD in dom p or ( DD in dom p & p . DD = TRUE ) )
by A27, A28, A31, A33, FUNCT_1:11, XXREAL_0:2;
suppose A39:
not
DD in dom p
;
( d in dom (iter (f,(i + 1))) & (iter (f,(i + 1))) . d in dom p & p . ((iter (f,(i + 1))) . d) = TRUE )A40:
DD in dom (PP_inversion p)
by A4, A39;
A41:
(PP_inversion p) . DD = TRUE
by A39, PARTPR_2:def 17;
then A42:
(PP_and (r,(PP_inversion p))) . DD = TRUE
by A35, A36, A40, PARTPR_1:18;
A43:
DD in dom (PP_and (r,(PP_inversion p)))
by A5, A35, A36, A40, A41;
A44:
f . DD in dom p
by A30, A38, FUNCT_7:71;
DD in dom f
by A29, A37, FUNCT_1:11;
then
p . (f . DD) = TRUE
by A2, A42, A43, A44, Th11;
hence
(
d in dom (iter (f,(i + 1))) &
(iter (f,(i + 1))) . d in dom p &
p . ((iter (f,(i + 1))) . d) = TRUE )
by A29, A30, A38, FUNCT_7:71;
verum end; suppose that A45:
DD in dom p
and A46:
p . DD = TRUE
;
( d in dom (iter (f,(i + 1))) & (iter (f,(i + 1))) . d in dom p & p . ((iter (f,(i + 1))) . d) = TRUE )thus
d in dom (iter (f,(i + 1)))
by A29;
( (iter (f,(i + 1))) . d in dom p & p . ((iter (f,(i + 1))) . d) = TRUE )thus
(iter (f,(i + 1))) . d in dom p
by A30;
p . ((iter (f,(i + 1))) . d) = TRUE A47:
DD in dom (PP_and (r,p))
by A3, A35, A36, A45, A46;
A48:
(PP_and (r,p)) . DD = TRUE
by A45, A35, A36, A46, PARTPR_1:18;
(
DD in dom f &
f . DD in dom p )
by A29, A30, A34, A37, FUNCT_1:11, FUNCT_1:13;
hence
p . ((iter (f,(i + 1))) . d) = TRUE
by A1, A37, A38, A47, A48, Th11;
verum end; end;
end; A49:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A25, A26);
0 + 1
<= n
by A24, NAT_1:13;
then reconsider n1 =
n - 1 as
Element of
NAT by INT_1:5;
set E =
(iter (f,n1)) . d;
A50:
d in dom (r * (iter (f,n1)))
by A10;
then A51:
d in dom (iter (f,n1))
by FUNCT_1:11;
iter (
f,
n1) is
BinominativeFunction of
D
by FUNCT_7:86;
then reconsider E =
(iter (f,n1)) . d as
Element of
D by A51, PARTFUN1:4;
A52:
E in dom r
by A50, FUNCT_1:11;
(r * (iter (f,n1))) . d = TRUE
by A10;
then A53:
r . E = TRUE
by A50, FUNCT_1:12;
A54:
f * (iter (f,n1)) = iter (
f,
(n1 + 1))
by FUNCT_7:71;
then A55:
f . E = (PP_while (r,f)) . d
by A13, A51, FUNCT_1:13;
A56:
E in dom f
by A14, A54, FUNCT_1:11;
p . ((PP_while (r,f)) . d) = TRUE
proof
n1 < n - 0
by XREAL_1:15;
per cases then
( not E in dom p or ( E in dom p & p . E = TRUE ) )
by A49, A51;
suppose A57:
not
E in dom p
;
p . ((PP_while (r,f)) . d) = TRUE then A58:
E in dom (PP_inversion p)
by A4;
A59:
(PP_inversion p) . E = TRUE
by A57, PARTPR_2:def 17;
then A60:
(PP_and (r,(PP_inversion p))) . E = TRUE
by A52, A53, A58, PARTPR_1:18;
E in dom (PP_and (r,(PP_inversion p)))
by A52, A53, A58, A59, A5;
hence
p . ((PP_while (r,f)) . d) = TRUE
by A2, A16, A55, A56, A60, Th11;
verum end; suppose A61:
(
E in dom p &
p . E = TRUE )
;
p . ((PP_while (r,f)) . d) = TRUE then A62:
(PP_and (r,p)) . E = TRUE
by A52, A53, PARTPR_1:18;
E in dom (PP_and (r,p))
by A3, A52, A53, A61;
hence
p . ((PP_while (r,f)) . d) = TRUE
by A1, A16, A55, A56, A62, Th11;
verum end; end;
end; hence
(PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE
by A17;
verum end; end; end; end;
end;
then
<*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> in SFHTs D
;
hence
<*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D
; verum