let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( <*(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 ; :: thesis: <*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; :: thesis: ( 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)) ; :: thesis: (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 ( (PP_while (r,f)) . d in dom (PP_not r) & (PP_not r) . ((PP_while (r,f)) . d) = FALSE ) ; :: thesis: (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE

hence (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE by A12, A13, A15, PARTPR_1:def 2; :: thesis: verum

end;

suppose ( (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 ) ; :: thesis: (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE

hence (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE by PARTPR_1:18; :: thesis: verum

end;

suppose that A16: (PP_while (r,f)) . d in dom p and
A17: p . ((PP_while (r,f)) . d) = FALSE ; :: thesis: (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 :: thesis: ( (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; :: thesis: verum

end;

per cases ( n = 0 or n > 0 ) by NAT_1:3;

suppose A22: n = 0 ; :: thesis: (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; :: thesis: verum

end;

suppose A24: n > 0 ; :: thesis: (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE

defpred S₁[ 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: S₁[ 0 ] by A21;
A26: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A27: S₁[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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;

suppose that A45: DD in dom p and
A46: p . DD = TRUE ; :: thesis: ( 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; :: thesis: ( (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; :: thesis: 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; :: thesis: verum

end;

end;

end;

A49: for k being Nat holds S₁[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 ; :: thesis: 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; :: thesis: verum

end;

suppose A61: ( E in dom p & p . E = TRUE ) ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE by A17; :: thesis: 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 ; :: thesis: verum