let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p, r being PartialPredicate of D st f coincides_with p & dom p c= dom f & <*(PP_and (r,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 f coincides_with p & dom p c= dom f & <*(PP_and (r,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: ( f coincides_with p & dom p c= dom f & <*(PP_and (r,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);
assume that
A1: f coincides_with p and
A2: dom p c= dom f and
A3: <*(PP_and (r,p)),f,p*> is SFHT of D ; :: thesis: <*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D
A4: 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;
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
A5: d in dom p and
A6: p . d = TRUE and
A7: d in dom (PP_while (r,f)) and
A8: (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
A9: for i being Nat st i <= n - 1 holds
( d in dom (r * (iter (f,i))) & (r * (iter (f,i))) . d = TRUE ) and
A10: d in dom (r * (iter (f,n))) and
A11: (r * (iter (f,n))) . d = FALSE and
A12: (PP_while (r,f)) . d = (iter (f,n)) . d by A7, PARTPR_2:def 15;
reconsider I = iter (f,n) as BinominativeFunction of D by FUNCT_7:86;
A13: d in dom I by A10, FUNCT_1:11;
A14: (r * I) . d = r . (I . d) by A10, 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 A8, 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 A11, A12, A14, 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 A15: (PP_while (r,f)) . d in dom p and
A16: p . ((PP_while (r,f)) . d) = FALSE ; :: thesis: (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE
for i being Nat st i <= n & d in dom (iter (f,i)) & (iter (f,i)) . d in dom p holds
p . ((iter (f,i)) . d) = TRUE
proof
defpred S1[ Nat] means ( $1 <= n implies for i being Nat st i <= $1 holds
( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE ) );
A17: S1[ 0 ]
proof
assume 0 <= n ; :: thesis: for i being Nat st i <= 0 holds
( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
let i be Nat; :: thesis: ( i <= 0 implies ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE ) )
assume A18: i <= 0 ; :: thesis: ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
A19: i = 0 by A18, NAT_1:3;
A20: iter (f,0) = id (field f) by FUNCT_7:68;
dom f c= field f by XBOOLE_1:7;
hence ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE ) by A2, A5, A6, A19, A20, FUNCT_1:18; :: thesis: verum
end;
A21: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume that
A22: S1[k] and
A23: k + 1 <= n ; :: thesis: for i being Nat st i <= k + 1 holds
( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
let i be Nat; :: thesis: ( i <= k + 1 implies ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE ) )
assume A24: i <= k + 1 ; :: thesis: ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
A25: k <= k + 1 by NAT_1:11;
per cases ( i <= k or i = k + 1 ) by A24, NAT_1:8;
suppose i <= k ; :: thesis: ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
hence ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE ) by A22, A23, A25, XXREAL_0:2; :: thesis: verum
end;
suppose A26: i = k + 1 ; :: thesis: ( (iter (f,i)) . d in dom p & d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
set DD = (iter (f,k)) . d;
A27: (k + 1) - 1 <= n - 1 by A23, XREAL_1:9;
A28: d in dom (r * (iter (f,k))) by A9, A27;
then A29: d in dom (iter (f,k)) by FUNCT_1:11;
iter (f,k) is BinominativeFunction of D by FUNCT_7:86;
then reconsider DD = (iter (f,k)) . d as Element of D by A29, PARTFUN1:4;
A30: DD in dom p by A22, A23, A25, XXREAL_0:2;
(r * (iter (f,k))) . d = TRUE by A9, A27;
then A31: r . DD = TRUE by A29, FUNCT_1:13;
A32: DD in dom r by A28, FUNCT_1:11;
A33: p . DD = TRUE by A22, A23, A25, XXREAL_0:2;
A34: DD in dom (PP_and (r,p)) by A4, A30, A31, A32, A33;
A35: (PP_and (r,p)) . DD = TRUE by A30, A31, A32, A33, PARTPR_1:18;
A36: iter (f,(k + 1)) = f * (iter (f,k)) by FUNCT_7:71;
A37: f . DD = (f * (iter (f,k))) . d by A29, FUNCT_1:13;
hence (iter (f,i)) . d in dom p by A1, A22, A23, A25, A26, A36, XXREAL_0:2; :: thesis: ( d in dom (iter (f,i)) & p . ((iter (f,i)) . d) = TRUE )
thus d in dom (iter (f,i)) by A2, A26, A29, A30, A36, FUNCT_1:11; :: thesis: p . ((iter (f,i)) . d) = TRUE
thus p . ((iter (f,i)) . d) = TRUE by A1, A3, A2, A26, A30, A34, A35, A37, A36, Th11; :: thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A17, A21);
 hence for i being Nat st i <= n & d in dom (iter (f,i)) & (iter (f,i)) . d in dom p holds
p . ((iter (f,i)) . d) = TRUE ; :: thesis: verum
end;
hence (PP_and ((PP_not r),p)) . ((PP_while (r,f)) . d) = TRUE by A12, A13, A15, A16; :: thesis: verum
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