:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko

::

:: Received June 29, 2018

:: Copyright (c) 2018-2021 Association of Mizar Users

definition

let D be set ;

let f be BinominativeFunction of D;

let p be PartialPredicate of D;

end;
let f be BinominativeFunction of D;

let p be PartialPredicate of D;

pred f coincides_with p means :: NOMIN_3:def 1

for d being Element of D st d in dom p holds

f . d in dom p;

for d being Element of D st d in dom p holds

f . d in dom p;

:: deftheorem defines coincides_with NOMIN_3:def 1 :

for D being set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds

( f coincides_with p iff for d being Element of D st d in dom p holds

f . d in dom p );

for D being set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds

( f coincides_with p iff for d being Element of D st d in dom p holds

f . d in dom p );

definition
end;

:: deftheorem defines coincide_with NOMIN_3:def 2 :

for D being set

for f, g being BinominativeFunction of D

for p, q being PartialPredicate of D holds

( f,g coincide_with p,q iff for d being Element of D st d in rng f & g . d in dom q holds

d in dom p );

for D being set

for f, g being BinominativeFunction of D

for p, q being PartialPredicate of D holds

( f,g coincide_with p,q iff for d being Element of D st d in rng f & g . d in dom q holds

d in dom p );

theorem :: NOMIN_3:1

theorem :: NOMIN_3:2

definition

let D be set ;

let p, q be PartialPredicate of D;

for p being PartialPredicate of D

for d being Element of D st d in dom p & p . d = TRUE holds

( d in dom p & p . d = TRUE ) ;

end;
let p, q be PartialPredicate of D;

pred p ||= q means :: NOMIN_3:def 3

for d being Element of D st d in dom p & p . d = TRUE holds

( d in dom q & q . d = TRUE );

reflexivity for d being Element of D st d in dom p & p . d = TRUE holds

( d in dom q & q . d = TRUE );

for p being PartialPredicate of D

for d being Element of D st d in dom p & p . d = TRUE holds

( d in dom p & p . d = TRUE ) ;

:: deftheorem defines ||= NOMIN_3:def 3 :

for D being set

for p, q being PartialPredicate of D holds

( p ||= q iff for d being Element of D st d in dom p & p . d = TRUE holds

( d in dom q & q . d = TRUE ) );

for D being set

for p, q being PartialPredicate of D holds

( p ||= q iff for d being Element of D st d in dom p & p . d = TRUE holds

( d in dom q & q . d = TRUE ) );

theorem Th3: :: NOMIN_3:3

for D being non empty set

for p, q, r being PartialPredicate of D st p ||= r holds

PP_and (p,q) ||= r

for p, q, r being PartialPredicate of D st p ||= r holds

PP_and (p,q) ||= r

proof end;

theorem :: NOMIN_3:4

theorem :: NOMIN_3:5

for D being non empty set

for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds

PP_and (p,r) ||= PP_and (q,s)

for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds

PP_and (p,r) ||= PP_and (q,s)

proof end;

theorem Th6: :: NOMIN_3:6

for D being non empty set

for p, q, r being PartialPredicate of D st PP_or (p,q) ||= r holds

p ||= r

for p, q, r being PartialPredicate of D st PP_or (p,q) ||= r holds

p ||= r

proof end;

theorem :: NOMIN_3:7

for D being non empty set

for p, q, r being PartialPredicate of D st p ||= PP_or (q,r) holds

for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds

( d in dom r & r . d = TRUE )

for p, q, r being PartialPredicate of D st p ||= PP_or (q,r) holds

for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds

( d in dom r & r . d = TRUE )

proof end;

theorem :: NOMIN_3:8

theorem :: NOMIN_3:9

for D being non empty set

for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds

PP_or (p,r) ||= PP_or (q,s)

for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds

PP_or (p,r) ||= PP_or (q,s)

proof end;

theorem :: NOMIN_3:10

definition

let D be non empty set ;

{ <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE } is set ;

end;
func SemanticFloydHoareTriples D -> set equals :: NOMIN_3:def 4

{ <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE } ;

coherence { <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE } ;

{ <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE } is set ;

:: deftheorem defines SemanticFloydHoareTriples NOMIN_3:def 4 :

for D being non empty set holds SemanticFloydHoareTriples D = { <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE } ;

for D being non empty set holds SemanticFloydHoareTriples D = { <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE } ;

theorem Th11: :: NOMIN_3:11

for D being non empty set

for f being BinominativeFunction of D

for p, q being PartialPredicate of D st <*p,f,q*> in SFHTs D holds

for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE

for f being BinominativeFunction of D

for p, q being PartialPredicate of D st <*p,f,q*> in SFHTs D holds

for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE

proof end;

theorem Th12: :: NOMIN_3:12

for D being non empty set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds <*{},f,p*> in SFHTs D

for f being BinominativeFunction of D

for p being PartialPredicate of D holds <*{},f,p*> in SFHTs D

proof end;

definition

let D be non empty set ;

mode SemanticFloydHoareTriple of D is Element of SemanticFloydHoareTriples D;

mode SFHT of D is Element of SFHTs D;

end;
mode SemanticFloydHoareTriple of D is Element of SemanticFloydHoareTriples D;

mode SFHT of D is Element of SFHTs D;

theorem Th14: :: NOMIN_3:14

for D being non empty set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds <*p,(id (field f)),p*> is SFHT of D

for f being BinominativeFunction of D

for p being PartialPredicate of D holds <*p,(id (field f)),p*> is SFHT of D

proof end;

:: CONS_1 rule

theorem Th15: :: NOMIN_3:15

for D being non empty set

for f being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & r ||= p holds

<*r,f,q*> is SFHT of D

for f being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & r ||= p holds

<*r,f,q*> is SFHT of D

proof end;

:: CONS_2 rule

theorem :: NOMIN_3:16

for D being non empty set

for f being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & q ||= r & dom r c= dom q holds

<*p,f,r*> is SFHT of D

for f being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & q ||= r & dom r c= dom q holds

<*p,f,r*> is SFHT of D

proof end;

:: skip rule

theorem Th18: :: NOMIN_3:18

for D being non empty set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds <*(PP_False D),f,p*> is SFHT of D

for f being BinominativeFunction of D

for p being PartialPredicate of D holds <*(PP_False D),f,p*> is SFHT of D

proof end;

theorem :: NOMIN_3:19

for D being non empty set

for f being BinominativeFunction of D

for p, q being PartialPredicate of D st p is total holds

<*(PP_inversion p),f,q*> is SFHT of D

for f being BinominativeFunction of D

for p, q being PartialPredicate of D st p is total holds

<*(PP_inversion p),f,q*> is SFHT of D

proof end;

theorem :: NOMIN_3:20

for D being non empty set

for f, g being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r holds

<*p,(PP_composition (f,g)),r*> is SFHT of D

for f, g being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r holds

<*p,(PP_composition (f,g)),r*> is SFHT of D

proof end;

:: IF rule

theorem :: NOMIN_3:21

for D being non empty set

for f, g being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*(PP_and (r,p)),f,q*> is SFHT of D & <*(PP_and ((PP_not r),p)),g,q*> is SFHT of D holds

<*p,(PP_IF (r,f,g)),q*> is SFHT of D

for f, g being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*(PP_and (r,p)),f,q*> is SFHT of D & <*(PP_and ((PP_not r),p)),g,q*> is SFHT of D holds

<*p,(PP_IF (r,f,g)),q*> is SFHT of D

proof end;

theorem :: NOMIN_3:22

for n being Nat

for D being non empty set

for f being BinominativeFunction of D

for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds

<*p,(iter (f,n)),p*> is SFHT of D

for D being non empty set

for f being BinominativeFunction of D

for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds

<*p,(iter (f,n)),p*> is SFHT of D

proof end;

:: while rule

theorem :: NOMIN_3:23

for D being non empty set

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

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

proof end;

theorem Th24: :: NOMIN_3:24

for D being non empty set

for f, g being BinominativeFunction of D

for p, q, r, s being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,s*> is SFHT of D holds

<*p,(PP_composition (f,g)),(PP_or (r,s))*> is SFHT of D

for f, g being BinominativeFunction of D

for p, q, r, s being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,s*> is SFHT of D holds

<*p,(PP_composition (f,g)),(PP_or (r,s))*> is SFHT of D

proof end;

theorem :: NOMIN_3:25

for D being non empty set

for f, g being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D holds

<*p,(PP_composition (f,g)),r*> is SFHT of D

for f, g being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D holds

<*p,(PP_composition (f,g)),r*> is SFHT of D

proof end;

theorem :: NOMIN_3:26

for D being 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

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

proof end;

:: DP rule

theorem :: NOMIN_3:27

for D being non empty set

for f being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D holds

<*(PP_or (p,q)),f,r*> is SFHT of D

for f being BinominativeFunction of D

for p, q, r being PartialPredicate of D st <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D holds

<*(PP_or (p,q)),f,r*> is SFHT of D

proof end;

theorem Th27: :: NOMIN_3:28

for V, A being set

for p, q being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A st ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE ) holds

<*p,f,q*> is SFHT of (ND (V,A))

for p, q being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A st ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds

q . (f . d) = TRUE ) holds

<*p,f,q*> is SFHT of (ND (V,A))

proof end;

theorem :: NOMIN_3:29

for v being object

for V, A being set

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))

for V, A being set

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))

proof end;

:: SFID_1 rule

theorem :: NOMIN_3:30

for v being object

for V, A being set

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A))

for V, A being set

for p being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A))

proof end;

:: SFID rule

theorem :: NOMIN_3:31

for V, A being set

for p being SCPartialNominativePredicate of V,A

for E being b_{1},b_{2} -FPrg-yielding FinSequence

for e being Element of product E st product E <> {} holds

<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))

for p being SCPartialNominativePredicate of V,A

for E being b

for e being Element of product E st product E <> {} holds

<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))

proof end;

:: SF_1 rule

theorem :: NOMIN_3:32

for v being object

for V, A being set

for p, q being SCPartialNominativePredicate of V,A

for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds

<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))

for V, A being set

for p, q being SCPartialNominativePredicate of V,A

for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds

<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))

proof end;

:: SF rule

theorem :: NOMIN_3:33

for V, A being set

for p, q being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A

for E being b_{1},b_{2} -FPrg-yielding FinSequence

for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds

<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))

for p, q being SCPartialNominativePredicate of V,A

for f being SCBinominativeFunction of V,A

for E being b

for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds

<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))

proof end;