MODELC_1: Model Checking, Part {I}

func CTL_WFF -> non empty set means :Def12: :: MODELC_1:def 12
( ( for a being set st a in it holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in it ) & ( for p being FinSequence of NAT st p in it holds
'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds
p '&' q in it ) & ( for p being FinSequence of NAT st p in it holds
EX p in it ) & ( for p being FinSequence of NAT st p in it holds
EG p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds
p EU q in it ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
it c= D ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines CTL_WFF MODELC_1:def 12 :

definition

let IT be FinSequence of NAT ;

attr IT is CTL-formula-like means :Def13: :: MODELC_1:def 13
IT is Element of CTL_WFF ;

end;

:: deftheorem Def13 defines CTL-formula-like MODELC_1:def 13 :

registration

cluster Relation-like NAT -defined NAT -valued Function-like FinSequence-like CTL-formula-like for FinSequence of NAT ;

existence

proof end;

end;

definition

mode CTL-formula is CTL-formula-like FinSequence of NAT ;

end;

theorem Th1: :: MODELC_1:1

for a being set holds
( a is CTL-formula iff a in CTL_WFF )

proof end;

registration

let n be Element of NAT ;

cluster atom. n -> CTL-formula-like ;

coherence by Def12;

end;

registration

let H be CTL-formula;

cluster 'not' H -> CTL-formula-like ;

coherence

proof end;

cluster EX H -> CTL-formula-like ;

coherence

proof end;

cluster EG H -> CTL-formula-like ;

coherence

proof end;

let G be CTL-formula;

cluster H '&' G -> CTL-formula-like ;

coherence

proof end;

cluster H EU G -> CTL-formula-like ;

coherence

proof end;

end;

definition

let H be CTL-formula;

attr H is atomic means :: MODELC_1:def 14
ex n being Element of NAT st H = atom. n;

attr H is negative means :: MODELC_1:def 15
ex H1 being CTL-formula st H = 'not' H1;

attr H is conjunctive means :: MODELC_1:def 16
ex F, G being CTL-formula st H = F '&' G;

attr H is ExistNext means :: MODELC_1:def 17
ex H1 being CTL-formula st H = EX H1;

attr H is ExistGlobal means :: MODELC_1:def 18
ex H1 being CTL-formula st H = EG H1;

attr H is ExistUntill means :: MODELC_1:def 19
ex F, G being CTL-formula st H = F EU G;

end;

:: deftheorem defines atomic MODELC_1:def 14 :

:: deftheorem defines negative MODELC_1:def 15 :

:: deftheorem defines conjunctive MODELC_1:def 16 :

:: deftheorem defines ExistNext MODELC_1:def 17 :

:: deftheorem defines ExistGlobal MODELC_1:def 18 :

:: deftheorem defines ExistUntill MODELC_1:def 19 :

definition

let F, G be CTL-formula;

func F 'or' G -> CTL-formula equals :: MODELC_1:def 20
'not' (('not' F) '&' ('not' G));

coherence ;

end;

:: deftheorem defines 'or' MODELC_1:def 20 :

theorem Th2: :: MODELC_1:2

for H being CTL-formula holds
( H is atomic or H is negative or H is conjunctive or H is ExistNext or H is ExistGlobal or H is ExistUntill )

proof end;

Lm3: for H being CTL-formula st H is negative holds
H . 1 = 0
by FINSEQ_1:41;

Lm4: for H being CTL-formula st H is conjunctive holds
H . 1 = 1

proof end;

Lm5: for H being CTL-formula st H is ExistNext holds
H . 1 = 2
by FINSEQ_1:41;

Lm6: for H being CTL-formula st H is ExistGlobal holds
H . 1 = 3
by FINSEQ_1:41;

Lm7: for H being CTL-formula st H is ExistUntill holds
H . 1 = 4

proof end;

Lm8: for H being CTL-formula st H is atomic holds
( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 )

proof end;

Lm9: for H being CTL-formula holds
( ( H is atomic & H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 ) or ( H is negative & H . 1 = 0 ) or ( H is conjunctive & H . 1 = 1 ) or ( H is ExistNext & H . 1 = 2 ) or ( H is ExistGlobal & H . 1 = 3 ) or ( H is ExistUntill & H . 1 = 4 ) )

proof end;

Lm10: for H being CTL-formula holds 1 <= len H

proof end;

Lm11: for F, H being CTL-formula
for sq being FinSequence st H = F ^ sq holds
H = F

proof end;

Lm12: for G, G1, H, H1 being CTL-formula st H '&' G = H1 '&' G1 holds
( H = H1 & G = G1 )

proof end;

Lm13: for G, G1, H, H1 being CTL-formula st H EU G = H1 EU G1 holds
( H = H1 & G = G1 )

proof end;

Lm14: for H being CTL-formula st H is atomic holds
( not H is negative & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )

proof end;

Lm15: for H being CTL-formula st H is negative holds
( not H is atomic & not H is conjunctive & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )

proof end;

Lm16: for H being CTL-formula st H is conjunctive holds
( not H is atomic & not H is negative & not H is ExistNext & not H is ExistGlobal & not H is ExistUntill )

proof end;

Lm17: for H being CTL-formula st H is ExistNext holds
( not H is atomic & not H is conjunctive & not H is negative & not H is ExistGlobal & not H is ExistUntill )

proof end;

Lm18: for H being CTL-formula st H is ExistGlobal holds
( not H is atomic & not H is conjunctive & not H is negative & not H is ExistNext & not H is ExistUntill )

proof end;

definition

let H be CTL-formula;
assume A1: ( H is negative or H is ExistNext or H is ExistGlobal ) ;

func the_argument_of H -> CTL-formula means :Def21: :: MODELC_1:def 21
'not' it = H if H is negative
EX it = H if H is ExistNext
otherwise EG it = H;

existence by A1;
uniqueness by FINSEQ_1:33;
consistency by Lm15;

end;

:: deftheorem Def21 defines the_argument_of MODELC_1:def 21 :

definition

let H be CTL-formula;
assume A1: ( H is conjunctive or H is ExistUntill ) ;

func the_left_argument_of H -> CTL-formula means :Def22: :: MODELC_1:def 22
ex H1 being CTL-formula st it '&' H1 = H if H is conjunctive
otherwise ex H1 being CTL-formula st it EU H1 = H;

existence by A1;
uniqueness by Lm12, Lm13;
consistency ;

func the_right_argument_of H -> CTL-formula means :Def23: :: MODELC_1:def 23
ex H1 being CTL-formula st H1 '&' it = H if H is conjunctive
otherwise ex H1 being CTL-formula st H1 EU it = H;

existence by A1;
uniqueness by Lm12, Lm13;
consistency ;

end;

:: deftheorem Def22 defines the_left_argument_of MODELC_1:def 22 :

:: deftheorem Def23 defines the_right_argument_of MODELC_1:def 23 :

Lm19: for H being CTL-formula st H is ExistGlobal holds
H = EG (the_argument_of H)

proof end;

Lm20: for H being CTL-formula st H is conjunctive holds
H = (the_left_argument_of H) '&' (the_right_argument_of H)

proof end;

Lm21: for H being CTL-formula st H is ExistUntill holds
H = (the_left_argument_of H) EU (the_right_argument_of H)

proof end;

Lm22: for H being CTL-formula st ( H is negative or H is ExistNext or H is ExistGlobal ) holds
len (the_argument_of H) < len H

proof end;

Lm23: for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds
( len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )

proof end;

definition

let x be object ;

func CastCTLformula x -> CTL-formula equals :Def24: :: MODELC_1:def 24
x if x in CTL_WFF
otherwise atom. 0;

correctness by Th1;

end;

:: deftheorem Def24 defines CastCTLformula MODELC_1:def 24 :

::***************************************************
::**
::** definition of Kripke structure & CTL model structure.
::**
::****************************************************

definition

let Prop be set ;
attr c₂ is strict ;
struct KripkeStr over Prop -> RelStr ;
aggr KripkeStr(# carrier, Starts, InternalRel, Label #) -> KripkeStr over Prop;
sel Starts c₂ -> Subset of the carrier of c₂;
sel Label c₂ -> Function of the carrier of c₂,(bool Prop);

end;

definition

attr c₁ is strict ;
struct CTLModelStr -> ComplULattStr ;
aggr CTLModelStr(# carrier, BasicAssign, L_meet, Compl, EneXt, EGlobal, EUntill #) -> CTLModelStr ;
sel BasicAssign c₁ -> Subset of the carrier of c₁;
sel EneXt c₁ -> UnOp of the carrier of c₁;
sel EGlobal c₁ -> UnOp of the carrier of c₁;
sel EUntill c₁ -> BinOp of the carrier of c₁;

end;

definition

let V be CTLModelStr ;
mode Assign of V is Element of the carrier of V;

end;

:: Preparation to define semantics for CTL-language
:: definition of evaluate function of CTL

definition

func atomic_WFF -> Subset of CTL_WFF equals :: MODELC_1:def 25
{ x where x is CTL-formula : x is atomic } ;

correctness

proof end;

end;

:: deftheorem defines atomic_WFF MODELC_1:def 25 :

definition

let V be CTLModelStr ;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let f be Function of CTL_WFF, the carrier of V;

pred f is-Evaluation-for Kai means :: MODELC_1:def 26
for H being CTL-formula holds
( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

end;

:: deftheorem defines is-Evaluation-for MODELC_1:def 26 :

definition

let V be CTLModelStr ;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let f be Function of CTL_WFF, the carrier of V;
let n be Nat;

pred f is-PreEvaluation-for n,Kai means :Def27: :: MODELC_1:def 27
for H being CTL-formula st len H <= n holds
( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) );

end;

:: deftheorem Def27 defines is-PreEvaluation-for MODELC_1:def 27 :

definition

let V be CTLModelStr ;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let f, h be Function of CTL_WFF, the carrier of V;
let n be Nat;
let H be CTL-formula;

func GraftEval (V,Kai,f,h,n,H) -> set equals :Def28: :: MODELC_1:def 28
f . H if len H > n + 1
Kai . H if ( len H = n + 1 & H is atomic )
the Compl of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is negative )
the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is conjunctive )
the EneXt of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is ExistNext )
the EGlobal of V . (h . (the_argument_of H)) if ( len H = n + 1 & H is ExistGlobal )
the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) if ( len H = n + 1 & H is ExistUntill )
h . H if len H < n + 1
otherwise {} ;

coherence ;
consistency by Lm14, Lm15, Lm16, Lm17, Lm18;

end;

:: deftheorem Def28 defines GraftEval MODELC_1:def 28 :

definition

let C be CTLModelStr ;

attr C is with_basic means :Def29: :: MODELC_1:def 29
not the BasicAssign of C is empty ;

end;

:: deftheorem Def29 defines with_basic MODELC_1:def 29 :

definition

func TrivialCTLModel -> CTLModelStr equals :: MODELC_1:def 30
CTLModelStr(# {0},([#] {0}),op2,op1,op1,op1,op2 #);

coherence ;

end;

:: deftheorem defines TrivialCTLModel MODELC_1:def 30 :

registration

cluster TrivialCTLModel -> non empty strict with_basic ;

coherence ;

end;

registration

cluster non empty for CTLModelStr ;

existence

proof end;

end;

registration

cluster non empty with_basic for CTLModelStr ;

existence

proof end;

end;

definition

mode CTLModel is non empty with_basic CTLModelStr ;

end;

registration

let C be CTLModel;

cluster the BasicAssign of C -> non empty ;

coherence by Def29;

end;

Lm24: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V holds f is-PreEvaluation-for 0 ,Kai
by Lm10;

Lm25: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V
for n being Nat st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai

proof end;

Lm26: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f1, f2 being Function of CTL_WFF, the carrier of V
for n being Nat st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H

proof end;

Lm27: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for n being Element of NAT ex f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai

proof end;

Lm28: for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V st ( for n being Element of NAT holds f is-PreEvaluation-for n,Kai ) holds
f is-Evaluation-for Kai

proof end;

definition

let V be CTLModel;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let n be Element of NAT ;

func EvalSet (V,Kai,n) -> non empty set equals :: MODELC_1:def 31
{ h where h is Function of CTL_WFF, the carrier of V : h is-PreEvaluation-for n,Kai } ;

correctness

proof end;

end;

:: deftheorem defines EvalSet MODELC_1:def 31 :

definition

let V be CTLModel;
let v0 be Element of the carrier of V;
let x be set ;

func CastEval (V,x,v0) -> Function of CTL_WFF, the carrier of V equals :Def32: :: MODELC_1:def 32
x if x in Funcs (CTL_WFF, the carrier of V)
otherwise CTL_WFF --> v0;

correctness by FUNCT_2:66;

end;

:: deftheorem Def32 defines CastEval MODELC_1:def 32 :

definition

let V be CTLModel;
let Kai be Function of atomic_WFF, the BasicAssign of V;

func EvalFamily (V,Kai) -> non empty set means :Def33: :: MODELC_1:def 33
for p being set holds
( p in it iff ( p in bool (Funcs (CTL_WFF, the carrier of V)) & ex n being Element of NAT st p = EvalSet (V,Kai,n) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def33 defines EvalFamily MODELC_1:def 33 :

Lm29: for n being Element of NAT
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds EvalSet (V,Kai,n) in EvalFamily (V,Kai)

proof end;

theorem Th3: :: MODELC_1:3

for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V ex f being Function of CTL_WFF, the carrier of V st f is-Evaluation-for Kai

proof end;

theorem Th4: :: MODELC_1:4

for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for f1, f2 being Function of CTL_WFF, the carrier of V st f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai holds
f1 = f2

proof end;

definition

let V be CTLModel;
let Kai be Function of atomic_WFF, the BasicAssign of V;
let H be CTL-formula;

func Evaluate (H,Kai) -> Assign of V means :Def34: :: MODELC_1:def 34
ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & it = f . H );

existence

proof end;

uniqueness by Th4;

end;

:: deftheorem Def34 defines Evaluate MODELC_1:def 34 :

notation

let V be CTLModel;
let f be Assign of V;
synonym 'not' f for f ` ;
let g be Assign of V;
synonym f '&' g for f "/\" g;

end;

definition

let V be CTLModel;
let f be Assign of V;

func EX f -> Assign of V equals :: MODELC_1:def 35
the EneXt of V . f;

correctness ;

func EG f -> Assign of V equals :: MODELC_1:def 36
the EGlobal of V . f;

correctness ;

end;

:: deftheorem defines EX MODELC_1:def 35 :

:: deftheorem defines EG MODELC_1:def 36 :

definition

let V be CTLModel;
let f, g be Assign of V;

func f EU g -> Assign of V equals :: MODELC_1:def 37
the EUntill of V . (f,g);

correctness ;

func f 'or' g -> Assign of V equals :: MODELC_1:def 38
'not' (('not' f) '&' ('not' g));

correctness ;

end;

:: deftheorem defines EU MODELC_1:def 37 :

:: deftheorem defines 'or' MODELC_1:def 38 :

::Some properties of evaluate function of CTL

theorem Th5: :: MODELC_1:5

for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate (('not' H),Kai) = 'not' (Evaluate (H,Kai))

proof end;

theorem Th6: :: MODELC_1:6

for H1, H2 being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 '&' H2),Kai) = (Evaluate (H1,Kai)) '&' (Evaluate (H2,Kai))

proof end;

theorem Th7: :: MODELC_1:7

for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EX H),Kai) = EX (Evaluate (H,Kai))

proof end;

theorem Th8: :: MODELC_1:8

for H being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((EG H),Kai) = EG (Evaluate (H,Kai))

proof end;

theorem Th9: :: MODELC_1:9

for H1, H2 being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 EU H2),Kai) = (Evaluate (H1,Kai)) EU (Evaluate (H2,Kai))

proof end;

theorem Th10: :: MODELC_1:10

for H1, H2 being CTL-formula
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V holds Evaluate ((H1 'or' H2),Kai) = (Evaluate (H1,Kai)) 'or' (Evaluate (H2,Kai))

proof end;

notation

let f be Function;
let n be Nat;
synonym f |** n for iter (f,n);

end;

definition

let S be set ;
let f be Function of S,S;
let n be Nat;
:: original: |**
redefine func f |** n -> Function of S,S;
coherence

proof end;

end;

Lm30: for S being set
for R being Relation of S,S st R is total holds
for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R )

proof end;

Lm31: for S being set
for R being Relation of S,S st ( for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ) holds
R is total

proof end;

Lm32: for S being non empty set
for R being total Relation of S,S
for s being Element of S holds not R .: {s} is empty

proof end;

:: scheme for path with condition F

scheme :: MODELC_1:sch 1
ExistPath{ F₁() -> non empty set , F₂() -> total Relation of F₁(),F₁(), F₃() -> Element of F₁(), F₄( Element of F₁()) -> set } :

ex f being sequence of F₁() st
( f . 0 = F₃() & ( for n being Element of NAT holds
( [(f . n),(f . (n + 1))] in F₂() & f . (n + 1) in F₄((f . n)) ) ) )

provided

A1: for s being Element of F₁() holds (Im (F₂(),s)) /\ F₄(s) is non empty Subset of F₁()

proof end;

Lm33: for S being non empty set
for R being total Relation of S,S
for s0 being Element of S ex f being sequence of S st
( f . 0 = s0 & ( for n being Nat holds [(f . n),(f . (n + 1))] in R ) )

proof end;

:: definition of infinity path

definition

let S be non empty set ;
let R be total Relation of S,S;

mode inf_path of R -> sequence of S means :Def39: :: MODELC_1:def 39
for n being Nat holds [(it . n),(it . (n + 1))] in R;

existence

proof end;

end;

:: deftheorem Def39 defines inf_path MODELC_1:def 39 :

::definition of concrete object of CTL model

definition

let S be non empty set ;

func ModelSP S -> set equals :: MODELC_1:def 40
Funcs (S,BOOLEAN);

correctness ;

end;

:: deftheorem defines ModelSP MODELC_1:def 40 :

registration

let S be non empty set ;

cluster ModelSP S -> non empty ;

coherence ;

end;

:: definition Fid:ModelSP(S) -> Function of S,BOOLEAN

definition

let S be non empty set ;
let f be object ;

func Fid (f,S) -> Function of S,BOOLEAN equals :Def41: :: MODELC_1:def 41
f if f in ModelSP S
otherwise S --> FALSE;

correctness by FUNCT_2:66;

end;

:: deftheorem Def41 defines Fid MODELC_1:def 41 :

Lm34: for S being non empty set
for s being Element of S
for f being set st (Fid (f,S)) . s <> TRUE holds
(Fid (f,S)) . s = FALSE
by TARSKI:def 2;

::schemes for existence & uniqueness of 1 Operand functor

scheme :: MODELC_1:sch 2
Func1EX{ F₁() -> non empty set , F₂() -> Function of F₁(),BOOLEAN, F₃( object , Function of F₁(),BOOLEAN) -> boolean object } :

ex g being set st
( g in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₃(s,F₂()) = TRUE iff (Fid (g,F₁())) . s = TRUE ) ) )

proof end;

scheme :: MODELC_1:sch 3
Func1Unique{ F₁() -> non empty set , F₂() -> Function of F₁(),BOOLEAN, F₃( object , Function of F₁(),BOOLEAN) -> boolean object } :

for g1, g2 being set st g1 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₃(s,F₂()) = TRUE iff (Fid (g1,F₁())) . s = TRUE ) ) & g2 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₃(s,F₂()) = TRUE iff (Fid (g2,F₁())) . s = TRUE ) ) holds
g1 = g2

proof end;

::schemes for existence & uniqueness of Unary Operation

scheme :: MODELC_1:sch 4
UnOpEX{ F₁() -> non empty set , F₂( object ) -> Element of F₁() } :

ex o being UnOp of F₁() st
for f being object st f in F₁() holds
o . f = F₂(f)

proof end;

scheme :: MODELC_1:sch 5
UnOpUnique{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> Element of F₂() } :

for o1, o2 being UnOp of F₂() st ( for f being object st f in F₂() holds
o1 . f = F₃(f) ) & ( for f being object st f in F₂() holds
o2 . f = F₃(f) ) holds
o1 = o2

proof end;

::schemes for existence & uniqueness of 2 Operands functor .

scheme :: MODELC_1:sch 6
Func2EX{ F₁() -> non empty set , F₂() -> Function of F₁(),BOOLEAN, F₃() -> Function of F₁(),BOOLEAN, F₄( object , Function of F₁(),BOOLEAN, Function of F₁(),BOOLEAN) -> boolean object } :

ex h being set st
( h in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h,F₁())) . s = TRUE ) ) )

proof end;

scheme :: MODELC_1:sch 7
Func2Unique{ F₁() -> non empty set , F₂() -> Function of F₁(),BOOLEAN, F₃() -> Function of F₁(),BOOLEAN, F₄( object , Function of F₁(),BOOLEAN, Function of F₁(),BOOLEAN) -> boolean object } :

for h1, h2 being set st h1 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h1,F₁())) . s = TRUE ) ) & h2 in ModelSP F₁() & ( for s being set st s in F₁() holds
( F₄(s,F₂(),F₃()) = TRUE iff (Fid (h2,F₁())) . s = TRUE ) ) holds
h1 = h2

proof end;

:: definition of Not_ unary operation of Model Space.

definition

let S be non empty set ;
let f be object ;

func Not_0 (f,S) -> Element of ModelSP S means :Def42: :: MODELC_1:def 42
for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (it,S)) . s = TRUE );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines Not_0 MODELC_1:def 42 :

Lm35: for S being non empty set
for o1, o2 being UnOp of (ModelSP S) st ( for f being object st f in ModelSP S holds
o1 . f = Not_0 (f,S) ) & ( for f being object st f in ModelSP S holds
o2 . f = Not_0 (f,S) ) holds
o1 = o2

proof end;

definition

let S be non empty set ;

func Not_ S -> UnOp of (ModelSP S) means :Def43: :: MODELC_1:def 43
for f being object st f in ModelSP S holds
it . f = Not_0 (f,S);

existence

proof end;

uniqueness by Lm35;

end;

:: deftheorem Def43 defines Not_ MODELC_1:def 43 :

:: definition of EneXt_ unary operation of Model Space.

definition

let S be non empty set ;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be object ;

func EneXt_univ (x,f,R) -> Element of BOOLEAN equals :Def44: :: MODELC_1:def 44
TRUE if ( x in S & ex pai being inf_path of R st
( pai . 0 = x & f . (pai . 1) = TRUE ) )
otherwise FALSE ;

correctness ;

end;

:: deftheorem Def44 defines EneXt_univ MODELC_1:def 44 :

definition

let S be non empty set ;
let R be total Relation of S,S;
let f be object ;

func EneXt_0 (f,R) -> Element of ModelSP S means :Def45: :: MODELC_1:def 45
for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def45 defines EneXt_0 MODELC_1:def 45 :

Lm36: for S being non empty set
for R being total Relation of S,S
for o1, o2 being UnOp of (ModelSP S) st ( for f being object st f in ModelSP S holds
o1 . f = EneXt_0 (f,R) ) & ( for f being object st f in ModelSP S holds
o2 . f = EneXt_0 (f,R) ) holds
o1 = o2

proof end;

definition

let S be non empty set ;
let R be total Relation of S,S;

func EneXt_ R -> UnOp of (ModelSP S) means :Def46: :: MODELC_1:def 46
for f being object st f in ModelSP S holds
it . f = EneXt_0 (f,R);

existence

proof end;

uniqueness by Lm36;

end;

:: deftheorem Def46 defines EneXt_ MODELC_1:def 46 :

:: definition of EGlobal_ unary operation of Model Space.

definition

let S be non empty set ;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be set ;

func EGlobal_univ (x,f,R) -> Element of BOOLEAN equals :Def47: :: MODELC_1:def 47
TRUE if ( x in S & ex pai being inf_path of R st
( pai . 0 = x & ( for n being Element of NAT holds f . (pai . n) = TRUE ) ) )
otherwise FALSE ;

correctness ;

end;

:: deftheorem Def47 defines EGlobal_univ MODELC_1:def 47 :

definition

let S be non empty set ;
let R be total Relation of S,S;
let f be object ;

func EGlobal_0 (f,R) -> Element of ModelSP S means :Def48: :: MODELC_1:def 48
for s being set st s in S holds
( EGlobal_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def48 defines EGlobal_0 MODELC_1:def 48 :

Lm37: for S being non empty set
for R being total Relation of S,S
for o1, o2 being UnOp of (ModelSP S) st ( for f being object st f in ModelSP S holds
o1 . f = EGlobal_0 (f,R) ) & ( for f being object st f in ModelSP S holds
o2 . f = EGlobal_0 (f,R) ) holds
o1 = o2

proof end;

definition

let S be non empty set ;
let R be total Relation of S,S;

func EGlobal_ R -> UnOp of (ModelSP S) means :Def49: :: MODELC_1:def 49
for f being object st f in ModelSP S holds
it . f = EGlobal_0 (f,R);

existence

proof end;

uniqueness by Lm37;

end;

:: deftheorem Def49 defines EGlobal_ MODELC_1:def 49 :

:: definition of And_ Binary Operation of Model Space.

definition

let S be non empty set ;
let f, g be set ;

func And_0 (f,g,S) -> Element of ModelSP S means :Def50: :: MODELC_1:def 50
for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (it,S)) . s = TRUE );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def50 defines And_0 MODELC_1:def 50 :

Lm38: for S being non empty set
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = And_0 (f,g,S) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = And_0 (f,g,S) ) holds
o1 = o2

proof end;

definition

let S be non empty set ;

func And_ S -> BinOp of (ModelSP S) means :Def51: :: MODELC_1:def 51
for f, g being set st f in ModelSP S & g in ModelSP S holds
it . (f,g) = And_0 (f,g,S);

existence

proof end;

uniqueness by Lm38;

end;

:: deftheorem Def51 defines And_ MODELC_1:def 51 :

:: definition of EUntill_ Binary Operation of Model Space.

definition

let S be non empty set ;
let R be total Relation of S,S;
let f, g be Function of S,BOOLEAN;
let x be set ;

func EUntill_univ (x,f,g,R) -> Element of BOOLEAN equals :Def52: :: MODELC_1:def 52
TRUE if ( x in S & ex pai being inf_path of R st
( pai . 0 = x & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
f . (pai . j) = TRUE ) & g . (pai . m) = TRUE ) ) )
otherwise FALSE ;

correctness ;

end;

:: deftheorem Def52 defines EUntill_univ MODELC_1:def 52 :

definition

let S be non empty set ;
let R be total Relation of S,S;
let f, g be set ;

func EUntill_0 (f,g,R) -> Element of ModelSP S means :Def53: :: MODELC_1:def 53
for s being set st s in S holds
( EUntill_univ (s,(Fid (f,S)),(Fid (g,S)),R) = TRUE iff (Fid (it,S)) . s = TRUE );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def53 defines EUntill_0 MODELC_1:def 53 :

Lm39: for S being non empty set
for R being total Relation of S,S
for o1, o2 being BinOp of (ModelSP S) st ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o1 . (f,g) = EUntill_0 (f,g,R) ) & ( for f, g being set st f in ModelSP S & g in ModelSP S holds
o2 . (f,g) = EUntill_0 (f,g,R) ) holds
o1 = o2

proof end;

definition

let S be non empty set ;
let R be total Relation of S,S;

func EUntill_ R -> BinOp of (ModelSP S) means :Def54: :: MODELC_1:def 54
for f, g being set st f in ModelSP S & g in ModelSP S holds
it . (f,g) = EUntill_0 (f,g,R);

existence

proof end;

uniqueness by Lm39;

end;

:: deftheorem Def54 defines EUntill_ MODELC_1:def 54 :

:: definition of concrete object of CTL model by ModelSP

definition

let S be non empty set ;
let X be non empty Subset of (ModelSP S);
let s be object ;

func F_LABEL (s,X) -> Subset of X means :Def55: :: MODELC_1:def 55
for x being object holds
( x in it iff ( x in X & ex f being Function of S,BOOLEAN st
( f = x & f . s = TRUE ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def55 defines F_LABEL MODELC_1:def 55 :

definition

let S be non empty set ;
let X be non empty Subset of (ModelSP S);

func Label_ X -> Function of S,(bool X) means :Def56: :: MODELC_1:def 56
for x being object st x in S holds
it . x = F_LABEL (x,X);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def56 defines Label_ MODELC_1:def 56 :

definition

let S be non empty set ;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of (ModelSP S);

func KModel (R,S0,Prop) -> KripkeStr over Prop equals :: MODELC_1:def 57
KripkeStr(# S,S0,R,(Label_ Prop) #);

coherence ;

end;

:: deftheorem defines KModel MODELC_1:def 57 :

registration

let S be non empty set ;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of (ModelSP S);

cluster the carrier of (KModel (R,S0,Prop)) -> non empty ;

coherence ;

end;

registration

let S be non empty set ;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of (ModelSP S);

cluster ModelSP the carrier of (KModel (R,S0,Prop)) -> non empty for Subset of (Funcs ( the carrier of (KModel (R,S0,Prop)),BOOLEAN));

coherence ;

end;

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);

func BASSModel (R,BASSIGN) -> CTLModelStr equals :: MODELC_1:def 58
CTLModelStr(# (ModelSP S),BASSIGN,(And_ S),(Not_ S),(EneXt_ R),(EGlobal_ R),(EUntill_ R) #);

coherence ;

end;

:: deftheorem defines BASSModel MODELC_1:def 58 :

registration

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);

cluster BASSModel (R,BASSIGN) -> non empty with_basic ;

coherence ;

end;

:: definition of correctness of Assign of BASSModel(R,BASSIGN)

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let s be Element of S;
let f be Assign of (BASSModel (R,BASSIGN));

pred s |= f means :Def59: :: MODELC_1:def 59
(Fid (f,S)) . s = TRUE ;

end;

:: deftheorem Def59 defines |= MODELC_1:def 59 :

notation

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let s be Element of S;
let f be Assign of (BASSModel (R,BASSIGN));
antonym s |/= f for s |= f;

end;

theorem Th11: :: MODELC_1:11

for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for a being Assign of (BASSModel (R,BASSIGN)) st a in BASSIGN holds
( s |= a iff a in (Label_ BASSIGN) . s )

proof end;

theorem Th12: :: MODELC_1:12

for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds
( s |= 'not' f iff s |/= f )

proof end;

theorem Th13: :: MODELC_1:13

proof end;

theorem Th14: :: MODELC_1:14

proof end;

theorem Th15: :: MODELC_1:15

proof end;

theorem Th16: :: MODELC_1:16

for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( s |= f EU g iff ex pai being inf_path of R st
( pai . 0 = s & ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g ) ) )

proof end;

theorem Th17: :: MODELC_1:17

proof end;

:: definition of correctness of CTL-formula & its basic properties.

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN));
let s be Element of S;
let H be CTL-formula;

pred s,kai |= H means :Def60: :: MODELC_1:def 60
s |= Evaluate (H,kai);

end;

:: deftheorem Def60 defines |= MODELC_1:def 60 :

notation

end;

theorem :: MODELC_1:18

for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )

proof end;

theorem :: MODELC_1:19

proof end;

theorem :: MODELC_1:20

proof end;

theorem :: MODELC_1:21

for H1, H2 being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= H1 'or' H2 iff ( s,kai |= H1 or s,kai |= H2 ) )

proof end;

theorem :: MODELC_1:22

for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )

proof end;

theorem :: MODELC_1:23

for H being CTL-formula
for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )

proof end;

theorem :: MODELC_1:24

proof end;

::Some basic theorems for external Mizar files.

theorem Th25: :: MODELC_1:25

for S being non empty set
for R being total Relation of S,S
for s0 being Element of S ex pai being inf_path of R st pai . 0 = s0

proof end;

theorem :: MODELC_1:26

for S being non empty set
for R being Relation of S,S holds
( R is total iff for x being set st x in S holds
ex y being set st
( y in S & [x,y] in R ) ) by Lm30, Lm31;

::*************
::
::Verification of the basic algorithm
:: for Model checking based on CTL.
::
::the basic algorithm is solver to get
:: {s where s is Element of S: s,kai|=H}
::
::*************

definition

let S be non empty set ;
let R be total Relation of S,S;
let s0 be Element of S;
let pai be inf_path of R;
let n be object ;

func PrePath (n,s0,pai) -> Element of S equals :Def61: :: MODELC_1:def 61
s0 if n = 0
otherwise pai . (k_nat ((k_nat n) - 1));

correctness ;

end;

:: deftheorem Def61 defines PrePath MODELC_1:def 61 :

theorem Th27: :: MODELC_1:27

for S being non empty set
for R being total Relation of S,S
for s0, s1 being Element of S st [s0,s1] in R holds
ex pai being inf_path of R st
( pai . 0 = s0 & pai . 1 = s1 )

proof end;

theorem Th28: :: MODELC_1:28

proof end;

:: definition of predecessor

definition

let S be non empty set ;
let R be total Relation of S,S;
let H be Subset of S;

func Pred (H,R) -> Subset of S equals :: MODELC_1:def 62
{ s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } ;

coherence

proof end;

end;

:: deftheorem defines Pred MODELC_1:def 62 :

:: definition of SIGMA

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f be Assign of (BASSModel (R,BASSIGN));

func SIGMA f -> Subset of S equals :: MODELC_1:def 63
{ s where s is Element of S : s |= f } ;

correctness

proof end;

end;

:: deftheorem defines SIGMA MODELC_1:def 63 :

Lm40: for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA f = { s where s is Element of S : (Fid (f,S)) . s = TRUE }

proof end;

Lm41: for X being non empty set
for f, g being Function of X,BOOLEAN st { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } holds
f = g

proof end;

Lm42: for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st Fid (f,S) = Fid (g,S) holds
f = g

proof end;

:: SIGMA is one to one.

theorem :: MODELC_1:29

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st SIGMA f = SIGMA g holds
f = g

proof end;

:: definition of Tau (inverse of SIGMA).

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let T be Subset of S;

func Tau (T,R,BASSIGN) -> Assign of (BASSModel (R,BASSIGN)) means :Def64: :: MODELC_1:def 64
for s being set st s in S holds
(Fid (it,S)) . s = (chi (T,S)) . s;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def64 defines Tau MODELC_1:def 64 :

:: Tau is one to one.

theorem :: MODELC_1:30

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for T1, T2 being Subset of S st Tau (T1,R,BASSIGN) = Tau (T2,R,BASSIGN) holds
T1 = T2

proof end;

:: Tau is on to.

theorem Th31: :: MODELC_1:31

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds Tau ((SIGMA f),R,BASSIGN) = f

proof end;

:: SIGMA is on to.

theorem Th32: :: MODELC_1:32

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for T being Subset of S holds SIGMA (Tau (T,R,BASSIGN)) = T

proof end;

:: SIGMA is homomorphism .

theorem Th33: :: MODELC_1:33

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( SIGMA ('not' f) = S \ (SIGMA f) & SIGMA (f '&' g) = (SIGMA f) /\ (SIGMA g) & SIGMA (f 'or' g) = (SIGMA f) \/ (SIGMA g) )

proof end;

:: Tau is monotonic.

theorem Th34: :: MODELC_1:34

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for G1, G2 being Subset of S st G1 c= G2 holds
for s being Element of S st s |= Tau (G1,R,BASSIGN) holds
s |= Tau (G2,R,BASSIGN)

proof end;

:: SIGMA is monotonic.

theorem Th35: :: MODELC_1:35

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f1, f2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= f1 holds
s |= f2 ) holds
SIGMA f1 c= SIGMA f2

proof end;

:: theorems for translation
:: problem of
:: (1)find status s st s |= EG(f)
:: (2)find status s st s |= f EU g
:: to "find fixpoint of some function of bool S -> bool S".
:: definition Fax(f,*):carrier ->carrier

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f, g be Assign of (BASSModel (R,BASSIGN));

func Fax (f,g) -> Assign of (BASSModel (R,BASSIGN)) equals :: MODELC_1:def 65
f '&' (EX g);

correctness ;

end;

:: deftheorem defines Fax MODELC_1:def 65 :

:: Fax(f,*) is monotonic.

theorem Th36: :: MODELC_1:36

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g1, g2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= g1 holds
s |= g2 ) holds
for s being Element of S st s |= Fax (f,g1) holds
s |= Fax (f,g2)

proof end;

::commutative
:: Fax(f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFaxTau(f,*)
::

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f be Assign of (BASSModel (R,BASSIGN));
let G be Subset of S;

func SigFaxTau (f,G,R,BASSIGN) -> Subset of S equals :: MODELC_1:def 66
SIGMA (Fax (f,(Tau (G,R,BASSIGN))));

coherence ;

end;

:: deftheorem defines SigFaxTau MODELC_1:def 66 :

:: SigFaxTau(f,*) is monotonic.

theorem Th37: :: MODELC_1:37

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for G1, G2 being Subset of S st G1 c= G2 holds
SigFaxTau (f,G1,R,BASSIGN) c= SigFaxTau (f,G2,R,BASSIGN)

proof end;

:: Some tools to treat path.

definition

let S be non empty set ;
let R be total Relation of S,S;
let pai be inf_path of R;
let k be Element of NAT ;

func PathShift (pai,k) -> inf_path of R means :Def67: :: MODELC_1:def 67
for n being Element of NAT holds it . n = pai . (n + k);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def67 defines PathShift MODELC_1:def 67 :

definition

let S be non empty set ;
let R be total Relation of S,S;
let pai1, pai2 be inf_path of R;
let n, k be Nat;

func PathChange (pai1,pai2,k,n) -> set equals :Def68: :: MODELC_1:def 68
pai1 . n if n < k
otherwise pai2 . (n - k);

correctness ;

end;

:: deftheorem Def68 defines PathChange MODELC_1:def 68 :

definition

let S be non empty set ;
let R be total Relation of S,S;
let pai1, pai2 be inf_path of R;
let k be Nat;

func PathConc (pai1,pai2,k) -> sequence of S means :Def69: :: MODELC_1:def 69
for n being Nat holds it . n = PathChange (pai1,pai2,k,n);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def69 defines PathConc MODELC_1:def 69 :

theorem Th38: :: MODELC_1:38

for S being non empty set
for R being total Relation of S,S
for pai1, pai2 being inf_path of R
for k being Element of NAT st pai1 . k = pai2 . 0 holds
PathConc (pai1,pai2,k) is inf_path of R

proof end;

:: EG(f) is fixpoint of Fax(f,*).

theorem Th39: :: MODELC_1:39

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for s being Element of S holds
( s |= EG f iff s |= Fax (f,(EG f)) )

proof end;

:: Existence path for fixpoint of Fax(f,*).

theorem Th40: :: MODELC_1:40

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for g being Assign of (BASSModel (R,BASSIGN))
for s0 being Element of S st s0 |= g & ( for s being Element of S st s |= g holds
s |= EX g ) holds
ex pai being inf_path of R st
( pai . 0 = s0 & ( for n being Nat holds pai . (In (n,NAT)) |= g ) )

proof end;

:: EG(f) is the maximum fixpoint of Fax(f,*)

theorem Th41: :: MODELC_1:41

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= g iff s |= Fax (f,g) ) ) holds
for s being Element of S st s |= g holds
s |= EG f

proof end;

:: definition of TransEG(f)::translated function for EG(f)

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f be Assign of (BASSModel (R,BASSIGN));

func TransEG f -> V230() Function of (bool S),(bool S) means :Def70: :: MODELC_1:def 70
for G being Subset of S holds it . G = SigFaxTau (f,G,R,BASSIGN);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def70 defines TransEG MODELC_1:def 70 :

:: fixpoint of TransEG(f)

theorem Th42: :: MODELC_1:42

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds
( ( for s being Element of S holds
( s |= g iff s |= Fax (f,g) ) ) iff SIGMA g is_a_fixpoint_of TransEG f )

proof end;

theorem :: MODELC_1:43

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EG f) = gfp (S,(TransEG f))

proof end;

:: definition Foax(g,f,*):carrier ->carrier

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f, g, h be Assign of (BASSModel (R,BASSIGN));

func Foax (g,f,h) -> Assign of (BASSModel (R,BASSIGN)) equals :: MODELC_1:def 71
g 'or' (Fax (f,h));

coherence ;

end;

:: deftheorem defines Foax MODELC_1:def 71 :

:: Foax(g,f,*) is monotonic.

theorem Th44: :: MODELC_1:44

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h1, h2 being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S st s |= h1 holds
s |= h2 ) holds
for s being Element of S st s |= Foax (g,f,h1) holds
s |= Foax (g,f,h2)

proof end;

::commutative
:: Foax(g,f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFoaxTau(g,f,*)
::

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f, g be Assign of (BASSModel (R,BASSIGN));
let H be Subset of S;

func SigFoaxTau (g,f,H,R,BASSIGN) -> Subset of S equals :: MODELC_1:def 72
SIGMA (Foax (g,f,(Tau (H,R,BASSIGN))));

coherence ;

end;

:: deftheorem defines SigFoaxTau MODELC_1:def 72 :

:: SigFoaxTau(g,f,*) is monotonic.

theorem Th45: :: MODELC_1:45

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN))
for H1, H2 being Subset of S st H1 c= H2 holds
SigFoaxTau (g,f,H1,R,BASSIGN) c= SigFoaxTau (g,f,H2,R,BASSIGN)

proof end;

:: f EU g is fixpoint of Foax(g,f,*).

theorem Th46: :: MODELC_1:46

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN))
for s being Element of S holds
( s |= f EU g iff s |= Foax (g,f,(f EU g)) )

proof end;

:: f EU g is the minimum fixpoint of Foax(g,f,*)

theorem Th47: :: MODELC_1:47

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (BASSModel (R,BASSIGN)) st ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) holds
for s being Element of S st s |= f EU g holds
s |= h

proof end;

:: definition of TransEU(f,g)::translated function for f EU g

definition

let S be non empty set ;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of (ModelSP S);
let f, g be Assign of (BASSModel (R,BASSIGN));

func TransEU (f,g) -> V230() Function of (bool S),(bool S) means :Def73: :: MODELC_1:def 73
for H being Subset of S holds it . H = SigFoaxTau (g,f,H,R,BASSIGN);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def73 defines TransEU MODELC_1:def 73 :

:: fixpoint of TransEU(f,g)

theorem Th48: :: MODELC_1:48

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (BASSModel (R,BASSIGN)) holds
( ( for s being Element of S holds
( s |= h iff s |= Foax (g,f,h) ) ) iff SIGMA h is_a_fixpoint_of TransEU (f,g) )

proof end;

theorem :: MODELC_1:49

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (f EU g) = lfp (S,(TransEU (f,g)))

proof end;

:: Solver for EX and TransEG,TransEU

theorem Th50: :: MODELC_1:50

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN)) holds SIGMA (EX f) = Pred ((SIGMA f),R)

proof end;

theorem :: MODELC_1:51

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEG f) . X = (SIGMA f) /\ (Pred (X,R))

proof end;

theorem :: MODELC_1:52

for S being non empty set
for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g being Assign of (BASSModel (R,BASSIGN))
for X being Subset of S holds (TransEU (f,g)) . X = (SIGMA g) \/ ((SIGMA f) /\ (Pred (X,R)))

proof end;