:: Sequent calculus, derivability, provability. Goedel's completeness theorem.
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

Lm1:  for X, A, B being set st X is Subset of (Funcs (A,B)) holds
X is Subset-Family of [:A,B:]
proofend;

Lm2:  for S being Language
for t1, t2 being termal string of S holds (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S
proofend;

::#####################################################################
::#Definitions and auxiliary lemmas
definition
let S be Language;
funcS -sequents  ->  set  equals :: FOMODEL4:def 1
 {  [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite  }  ;
coherence
  {  [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite  }  is set ;
end;

:: deftheorem  defines -sequents FOMODEL4:def_1_:_
 for S being Language holds S -sequents =  {  [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite  }  ;

registration
let S be Language;
clusterS -sequents  ->  non empty ;
coherence
 not S -sequents is empty
proofend;
end;

registration
let S be Language;
clusterS -sequents  ->  Relation-like ;
coherence
 S -sequents is Relation-like
proofend;
end;

definition
let S be Language;
let x be set ;
attrx is S -sequent-like  means :Def2: :: FOMODEL4:def 2
x in S -sequents ;
end;

:: deftheorem Def2 defines -sequent-like FOMODEL4:def_2_:_
 for S being Language
for x being set holds
( x is S -sequent-like iff x in S -sequents );

definition
let S be Language;
let X be set ;
attrX is S -sequents-like  means :Def3: :: FOMODEL4:def 3
X c= S -sequents ;
end;

:: deftheorem Def3 defines -sequents-like FOMODEL4:def_3_:_
 for S being Language
for X being set holds
( X is S -sequents-like iff X c= S -sequents );

registration
let S be Language;
cluster  -> S -sequents-like for Element of bool (S -sequents);
coherence
 for b1 being Subset of (S -sequents) holds b1 is S -sequents-like by Def3;
cluster  -> S -sequent-like for Element of S -sequents ;
coherence
 for b1 being Element of S -sequents holds b1 is S -sequent-like by Def2;
end;

registration
let S be Language;
clusterS -sequent-like for Element of S -sequents ;
existence
 ex b1 being Element of S -sequents st b1 is S -sequent-like
proofend;
cluster Relation-like S -sequents-like for Element of bool (S -sequents);
existence
 ex b1 being Subset of (S -sequents) st b1 is S -sequents-like
proofend;
end;

registration
let S be Language;
clusterS -sequent-like for set ;
existence
 ex b1 being set st b1 is S -sequent-like
proofend;
clusterS -sequents-like for set ;
existence
 ex b1 being set st b1 is S -sequents-like
proofend;
end;

definition
let S be Language;
mode Rule of S is Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));
end;

definition
let S be Language;
mode RuleSet of S is Subset of (Funcs ((bool (S -sequents)),(bool (S -sequents))));
end;

registration
let A, B be set ;
let X be Subset of (Funcs (A,B));
cluster union X ->  Relation-like ;
coherence
 union X is Relation-like ;
end;

registration
let S be Language;
let D be RuleSet of S;
cluster union D ->  Relation-like ;
coherence
 union D is Relation-like ;
end;

definition
let S be Language;
let D be RuleSet of S;
func OneStep D ->  Rule of S means :Def4: :: FOMODEL4:def 4
 for Seqs being Element of bool (S -sequents) holds it . Seqs = union ((union D) .: {Seqs});
existence
 ex b1 being Rule of S st
for Seqs being Element of bool (S -sequents) holds b1 . Seqs = union ((union D) .: {Seqs})
proofend;
uniqueness
 for b1, b2 being Rule of S st ( for Seqs being Element of bool (S -sequents) holds b1 . Seqs = union ((union D) .: {Seqs}) ) &amp; ( for Seqs being Element of bool (S -sequents) holds b2 . Seqs = union ((union D) .: {Seqs}) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines OneStep FOMODEL4:def_4_:_
 for S being Language
for D being RuleSet of S
for b3 being Rule of S holds
( b3 = OneStep D iff for Seqs being Element of bool (S -sequents) holds b3 . Seqs = union ((union D) .: {Seqs}) );

Lm3:  for m being Nat
for S being Language
for D being RuleSet of S
for R being Rule of S
for Seqts being Subset of (S -sequents)
for SQ being b2 -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) &amp; rng (OneStep D) c= dom (OneStep D) &amp; iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) &amp; dom (iter ((OneStep D),m)) = bool (S -sequents) &amp; (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) &amp; Seqts in dom R &amp; SQ in dom (iter (R,m)) )
proofend;

definition
let S be Language;
let D be RuleSet of S;
let m be Nat;
func(m,D) -derivables  ->  Rule of S equals :: FOMODEL4:def 5
 iter ((OneStep D),m);
coherence
 iter ((OneStep D),m) is Rule of S
proofend;
end;

:: deftheorem  defines -derivables FOMODEL4:def_5_:_
 for S being Language
for D being RuleSet of S
for m being Nat holds (m,D) -derivables = iter ((OneStep D),m);

definition
let S be Language;
let D be RuleSet of S;
let Seqs1, Seqs2 be set ;
attrSeqs2 is Seqs1,D -derivable  means :Def6: :: FOMODEL4:def 6
Seqs2 c= union (((OneStep D) [*]) .: {Seqs1});
end;

:: deftheorem Def6 defines -derivable FOMODEL4:def_6_:_
 for S being Language
for D being RuleSet of S
for Seqs1, Seqs2 being set holds
( Seqs2 is Seqs1,D -derivable iff Seqs2 c= union (((OneStep D) [*]) .: {Seqs1}) );

definition
let m be Nat;
let S be Language;
let D be RuleSet of S;
let Seqts, seqt be set ;
attrseqt is m,Seqts,D -derivable  means :Def7: :: FOMODEL4:def 7
seqt in ((m,D) -derivables) . Seqts;
end;

:: deftheorem Def7 defines -derivable FOMODEL4:def_7_:_
 for m being Nat
for S being Language
for D being RuleSet of S
for Seqts, seqt being set holds
( seqt is m,Seqts,D -derivable iff seqt in ((m,D) -derivables) . Seqts );

definition
let S be Language;
let D be RuleSet of S;
funcD -iterators  ->  Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):] equals :: FOMODEL4:def 8
 {  (iter ((OneStep D),mm)) where mm is Element of NAT : verum  }  ;
coherence
  {  (iter ((OneStep D),mm)) where mm is Element of NAT : verum  }  is Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):]
proofend;
end;

:: deftheorem  defines -iterators FOMODEL4:def_8_:_
 for S being Language
for D being RuleSet of S holds D -iterators =  {  (iter ((OneStep D),mm)) where mm is Element of NAT : verum  }  ;

definition
let S be Language;
let R be Rule of S;
attrR is isotone  means :Def9: :: FOMODEL4:def 9
 for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 holds
R . Seqts1 c= R . Seqts2;
end;

:: deftheorem Def9 defines isotone FOMODEL4:def_9_:_
 for S being Language
for R being Rule of S holds
( R is isotone iff for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 holds
R . Seqts1 c= R . Seqts2 );

Lm4:  for S being Language
for R being Rule of S holds
( id (bool (S -sequents)) is Rule of S &amp; ( R = id (bool (S -sequents)) implies R is isotone ) )
proofend;

registration
let S be Language;
cluster Relation-like bool (S -sequents) -defined bool (S -sequents) -valued Function-like total quasi_total isotone for Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));
existence
 ex b1 being Rule of S st b1 is isotone
proofend;
end;

definition
let S be Language;
let D be RuleSet of S;
attrD is isotone  means :Def10: :: FOMODEL4:def 10
 for Seqts1, Seqts2 being Subset of (S -sequents)
for f being Function st Seqts1 c= Seqts2 &amp; f in D holds
ex g being Function st
( g in D &amp; f . Seqts1 c= g . Seqts2 );
end;

:: deftheorem Def10 defines isotone FOMODEL4:def_10_:_
 for S being Language
for D being RuleSet of S holds
( D is isotone iff for Seqts1, Seqts2 being Subset of (S -sequents)
for f being Function st Seqts1 c= Seqts2 &amp; f in D holds
ex g being Function st
( g in D &amp; f . Seqts1 c= g . Seqts2 ) );

registration
let S be Language;
let M be isotone Rule of S;
cluster{M} ->  isotone for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = {M} holds
b1 is isotone
proofend;
end;

registration
let S be Language;
cluster functional isotone for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being RuleSet of S st b1 is isotone
proofend;
end;

definition
let S be Language;
let D be RuleSet of S;
let Seqts be set ;
attrSeqts is D -derivable  means :Def11: :: FOMODEL4:def 11
Seqts is {} ,D -derivable ;
end;

:: deftheorem Def11 defines -derivable FOMODEL4:def_11_:_
 for S being Language
for D being RuleSet of S
for Seqts being set holds
( Seqts is D -derivable iff Seqts is {} ,D -derivable );

registration
let S be Language;
let D be RuleSet of S;
clusterD -derivable  ->  {} ,D -derivable for set ;
coherence
 for b1 being set st b1 is D -derivable holds
b1 is {} ,D -derivable by Def11;
cluster {} ,D -derivable  -> D -derivable for set ;
coherence
 for b1 being set st b1 is {} ,D -derivable holds
b1 is D -derivable by Def11;
end;

registration
let S be Language;
let D be RuleSet of S;
let Seqts be empty set ;
clusterSeqts,D -derivable  -> D -derivable for set ;
coherence
 for b1 being set st b1 is Seqts,D -derivable holds
b1 is D -derivable ;
end;

definition
let S be Language;
let D be RuleSet of S;
let X, phi be set ;
attrphi is X,D -provable  means :Def12: :: FOMODEL4:def 12
( {[X,phi]} is D -derivable or ex seqt being set st
( seqt `1 c= X &amp; seqt `2 = phi &amp; {seqt} is D -derivable ) );
end;

:: deftheorem Def12 defines -provable FOMODEL4:def_12_:_
 for S being Language
for D being RuleSet of S
for X, phi being set holds
( phi is X,D -provable iff ( {[X,phi]} is D -derivable or ex seqt being set st
( seqt `1 c= X &amp; seqt `2 = phi &amp; {seqt} is D -derivable ) ) );

definition
let S be Language;
let D be RuleSet of S;
let X, x be set ;
redefine attr x is X,D -provable  means :Def13: :: FOMODEL4:def 13
 ex seqt being set st
( seqt `1 c= X &amp; seqt `2 = x &amp; {seqt} is D -derivable );
compatibility
 ( x is X,D -provable iff ex seqt being set st
( seqt `1 c= X &amp; seqt `2 = x &amp; {seqt} is D -derivable ) )
proofend;
end;

:: deftheorem Def13 defines -provable FOMODEL4:def_13_:_
 for S being Language
for D being RuleSet of S
for X, x being set holds
( x is X,D -provable iff ex seqt being set st
( seqt `1 c= X &amp; seqt `2 = x &amp; {seqt} is D -derivable ) );

definition
let S be Language;
let D be RuleSet of S;
let R be Rule of S;
attrR is D -macro  means :: FOMODEL4:def 14
 for Seqs being Subset of (S -sequents) holds R . Seqs is Seqs,D -derivable ;
end;

:: deftheorem  defines -macro FOMODEL4:def_14_:_
 for S being Language
for D being RuleSet of S
for R being Rule of S holds
( R is D -macro iff for Seqs being Subset of (S -sequents) holds R . Seqs is Seqs,D -derivable );

definition
let S be Language;
let D be RuleSet of S;
let Phi be set ;
func(Phi,D) -termEq  ->  set  equals :: FOMODEL4:def 15
 {  [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable  }  ;
coherence
  {  [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable  }  is set ;
end;

:: deftheorem  defines -termEq FOMODEL4:def_15_:_
 for S being Language
for D being RuleSet of S
for Phi being set holds (Phi,D) -termEq =  {  [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable  }  ;

definition
let S be Language;
let D be RuleSet of S;
let Phi be set ;
attrPhi is D -expanded  means :Def16: :: FOMODEL4:def 16
 for x being set st x is Phi,D -provable holds
{x} c= Phi;
end;

:: deftheorem Def16 defines -expanded FOMODEL4:def_16_:_
 for S being Language
for D being RuleSet of S
for Phi being set holds
( Phi is D -expanded iff for x being set st x is Phi,D -provable holds
{x} c= Phi );

definition
let S be Language;
let x be set ;
attrx is S -null  means :Def17: :: FOMODEL4:def 17
verum;
end;

:: deftheorem Def17 defines -null FOMODEL4:def_17_:_
 for S being Language
for x being set holds
( x is S -null iff verum );

Lm5:  for X, Y, x being set
for S being Language
for D being RuleSet of S st X c= Y &amp; x is X,D -provable holds
x is Y,D -provable
proofend;

::#####################################################################
::#####################################################################
::#####################################################################
::#Type Tuning
definition
let S be Language;
let D be RuleSet of S;
let Phi be set ;
:: original:-termEq
redefine func(Phi,D) -termEq  ->  Relation of (AllTermsOf S);
coherence
 (Phi,D) -termEq is Relation of (AllTermsOf S)
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
let Phi1, Phi2 be finite Subset of (AllFormulasOf S);
cluster[(Phi1 \/ Phi2),phi] -> S -sequent-like ;
coherence
 [(Phi1 \/ Phi2),phi] is S -sequent-like
proofend;
end;

definition
let S be Language;
let x be empty set ;
let phi be wff string of S;
:: original:[
redefine func[x,phi] ->  Element of S -sequents ;
coherence
 [x,phi] is Element of S -sequents
proofend;
end;

registration
let S be Language;
cluster{} /\ S -> S -sequents-like for set ;
coherence
 for b1 being set st b1 = {} /\ S holds
b1 is S -sequents-like
proofend;
end;

registration
let S be Language;
clusterS -null for set ;
existence
 ex b1 being set st b1 is S -null by Def17;
end;

registration
let S be Language;
clusterS -sequent-like  -> S -null for set ;
coherence
 for b1 being set st b1 is S -sequent-like holds
b1 is S -null by Def17;
end;

registration
let S be Language;
cluster  -> S -null for Element of S -sequents ;
coherence
 for b1 being Element of S -sequents holds b1 is S -null ;
end;

registration
let m be Nat;
let S be Language;
let D be RuleSet of S;
let X be set ;
cluster((m,D) -derivables) . X -> S -sequents-like ;
coherence
 ((m,D) -derivables) . X is S -sequents-like
proofend;
end;

registration
let S be Language;
let Y be set ;
let X be S -sequents-like set ;
clusterX /\ Y -> S -sequents-like for set ;
coherence
 for b1 being set st b1 = X /\ Y holds
b1 is S -sequents-like
proofend;
end;

registration
let S be Language;
let D be RuleSet of S;
let m be Nat;
let X be set ;
clusterm,X,D -derivable  -> S -sequent-like for set ;
coherence
 for b1 being set st b1 is m,X,D -derivable holds
b1 is S -sequent-like
proofend;
end;

registration
let S be Language;
let D be RuleSet of S;
let Phi1, Phi2 be set ;
clusterPhi1 \ Phi2,D -provable  -> Phi1,D -provable for set ;
coherence
 for b1 being set st b1 is Phi1 \ Phi2,D -provable holds
b1 is Phi1,D -provable by Lm5;
end;

registration
let S be Language;
let D be RuleSet of S;
let Phi1, Phi2 be set ;
clusterPhi1 \ Phi2,D -provable  -> Phi1 \/ Phi2,D -provable for set ;
coherence
 for b1 being set st b1 is Phi1 \ Phi2,D -provable holds
b1 is Phi1 \/ Phi2,D -provable by Lm5, XBOOLE_1:7;
end;

registration
let S be Language;
let D be RuleSet of S;
let Phi1, Phi2 be set ;
clusterPhi1 /\ Phi2,D -provable  -> Phi1,D -provable for set ;
coherence
 for b1 being set st b1 is Phi1 /\ Phi2,D -provable holds
b1 is Phi1,D -provable by Lm5;
end;

registration
let S be Language;
let D be RuleSet of S;
let X be set ;
let x be Subset of X;
clusterx,D -provable  -> X,D -provable for set ;
coherence
 for b1 being set st b1 is x,D -provable holds
b1 is X,D -provable
proofend;
end;

registration
let S be Language;
let premises be finite Subset of (AllFormulasOf S);
let phi be wff string of S;
cluster[premises,phi] -> S -sequent-like for set ;
coherence
 for b1 being set st b1 = [premises,phi] holds
b1 is S -sequent-like
proofend;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster[{phi1},phi2] -> S -sequent-like for set ;
coherence
 for b1 being set st b1 = [{phi1},phi2] holds
b1 is S -sequent-like
proofend;
let phi3 be wff string of S;
cluster[{phi1,phi2},phi3] -> S -sequent-like for set ;
coherence
 for b1 being set st b1 = [{phi1,phi2},phi3] holds
b1 is S -sequent-like
proofend;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
let Phi be finite Subset of (AllFormulasOf S);
cluster[(Phi \/ {phi1}),phi2] -> S -sequent-like for set ;
coherence
 for b1 being set st b1 = [(Phi \/ {phi1}),phi2] holds
b1 is S -sequent-like
proofend;
end;

Lm6:  for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents holds
(OneStep D) . X = union (union  {  (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D  }  )
proofend;

Lm7:  for S being Language
for R being Rule of S holds R = OneStep {R}
proofend;

Lm8:  for y being set
for S being Language
for D being RuleSet of S
for Seqts being Subset of (S -sequents) st {y} is Seqts,D -derivable holds
ex mm being Element of NAT st y is mm,Seqts,D -derivable
proofend;

Lm9:  for m being Nat
for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
proofend;

Lm10:  for X being set
for S being Language
for D being RuleSet of S holds union (((OneStep D) [*]) .: {X}) = union  {  (((mm,D) -derivables) . X) where mm is Element of NAT : verum  }
proofend;

Lm11:  for m being Nat
for X being set
for S being Language
for D being RuleSet of S holds ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
proofend;

Lm12:  for m being Nat
for x, X being set
for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable
proofend;

Lm13:  for S being Language
for D1, D2 being RuleSet of S
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 &amp; D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) holds
(OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2
proofend;

Lm14:  for m being Nat
for S being Language
for D1, D2 being RuleSet of S
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 &amp; D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2
proofend;

Lm15:  for m being Nat
for S being Language
for D1, D2 being RuleSet of S
for SQ1, SQ2 being b2 -sequents-like set st SQ1 c= SQ2 &amp; D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2
proofend;

Lm16:  for m being Nat
for X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . X c= ((m,D2) -derivables) . X
proofend;

Lm17:  for X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) holds
union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})
proofend;

Lm18:  for Y, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) &amp; Y is X,D1 -derivable holds
Y is X,D2 -derivable
proofend;

Lm19:  for Y being set
for S being Language
for R being Rule of S
for Seqts being Subset of (S -sequents) st Y c= R . Seqts holds
Y is Seqts,{R} -derivable
proofend;

Lm20:  for m, n being Nat
for Z being set
for S being Language
for D1, D2 being RuleSet of S
for SQ2, SQ1 being b4 -sequents-like set st D1 is isotone &amp; D1 \/ D2 is isotone &amp; SQ2 c= (iter ((OneStep D1),m)) . SQ1 &amp; Z c= (iter ((OneStep D2),n)) . SQ2 holds
Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1
proofend;

Lm21:  for m, n being Nat
for y, X, z being set
for S being Language
for D1, D2 being RuleSet of S st D1 is isotone &amp; D1 \/ D2 is isotone &amp; y is m,X,D1 -derivable &amp; z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable
proofend;

Lm22:  for X being set
for S being Language
for t1, t2 being termal string of S
for D being RuleSet of S holds
( [t1,t2] in (X,D) -termEq iff (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable )
proofend;

Lm23:  for S being Language
for Sq being b1 -sequent-like set holds Sq `2 is wff string of S
proofend;

Lm24:  for x, X being set
for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S
proofend;

Lm25:  for S being Language
for D being RuleSet of S holds AllFormulasOf S is D -expanded
proofend;

registration
let S be Language;
let D be RuleSet of S;
cluster functional V36() FinSequence-membered with_non-empty_elements D -expanded for Element of bool (AllFormulasOf S);
existence
 ex b1 being Subset of (AllFormulasOf S) st b1 is D -expanded
proofend;
end;

registration
let S be Language;
let D be RuleSet of S;
clusterD -expanded for set ;
existence
 ex b1 being set st b1 is D -expanded
proofend;
end;

::############################################################################
::# Encoding of modified Gentzen rules
definition
let Seqts be set ;
let S be Language;
let seqt be S -null set ;
predseqt Rule0 Seqts means :Def18: :: FOMODEL4:def 18
seqt `2 in seqt `1 ;
predseqt Rule1 Seqts means :Def19: :: FOMODEL4:def 19
 ex y being set st
( y in Seqts &amp; y `1 c= seqt `1 &amp; seqt `2 = y `2 );
predseqt Rule2 Seqts means :Def20: :: FOMODEL4:def 20
( seqt `1 is empty &amp; ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t );
predseqt Rule3a Seqts means :Def21: :: FOMODEL4:def 21
 ex t, t1, t2 being termal string of S ex x being set st
( x in Seqts &amp; seqt `1 = (x `1) \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} &amp; x `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t1 &amp; seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 );
predseqt Rule3b Seqts means :Def22: :: FOMODEL4:def 22
 ex t1, t2 being termal string of S st
( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} &amp; seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 );
predseqt Rule3d Seqts means :Def23: :: FOMODEL4:def 23
 ex s being low-compounding Element of S ex T, U being abs (ar b1) -element Element of (AllTermsOf S) * st
( s is operational &amp; seqt `1 =  {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  &amp; seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) );
predseqt Rule3e Seqts means :Def24: :: FOMODEL4:def 24
 ex s being relational Element of S ex T, U being abs (ar b1) -element Element of (AllTermsOf S) * st
( seqt `1 = {(s -compound T)} \/  {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  &amp; seqt `2 = s -compound U );
predseqt Rule4 Seqts means :Def25: :: FOMODEL4:def 25
 ex l being literal Element of S ex phi being wff string of S ex t being termal string of S st
( seqt `1 = {((l,t) SubstIn phi)} &amp; seqt `2 = <*l*> ^ phi );
predseqt Rule5 Seqts means :Def26: :: FOMODEL4:def 26
 ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st
( seqt `1 = x \/ {(<*v1*> ^ p)} &amp; v2 is (x \/ {p}) \/ {(seqt `2)} -absent &amp; [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts );
predseqt Rule6 Seqts means :Def27: :: FOMODEL4:def 27
 ex y1, y2 being set ex phi1, phi2 being wff string of S st
( y1 in Seqts &amp; y2 in Seqts &amp; y1 `1 = y2 `1 &amp; y2 `1 = seqt `1 &amp; y1 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi1 &amp; y2 `2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi2 &amp; seqt `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 );
predseqt Rule7 Seqts means :Def28: :: FOMODEL4:def 28
 ex y being set ex phi1, phi2 being wff string of S st
( y in Seqts &amp; y `1 = seqt `1 &amp; y `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; seqt `2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi1 );
predseqt Rule8 Seqts means :Def29: :: FOMODEL4:def 29
 ex y1, y2 being set ex phi, phi1, phi2 being wff string of S st
( y1 in Seqts &amp; y2 in Seqts &amp; y1 `1 = y2 `1 &amp; y1 `2 = phi1 &amp; y2 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; {phi} \/ (seqt `1) = y1 `1 &amp; seqt `2 = (<*(TheNorSymbOf S)*> ^ phi) ^ phi );
predseqt Rule9 Seqts means :Def30: :: FOMODEL4:def 30
 ex y being set ex phi being wff string of S st
( y in Seqts &amp; seqt `2 = phi &amp; y `1 = seqt `1 &amp; y `2 = xnot (xnot phi) );
end;

:: deftheorem Def18 defines Rule0 FOMODEL4:def_18_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule0 Seqts iff seqt `2 in seqt `1 );

:: deftheorem Def19 defines Rule1 FOMODEL4:def_19_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule1 Seqts iff ex y being set st
( y in Seqts &amp; y `1 c= seqt `1 &amp; seqt `2 = y `2 ) );

:: deftheorem Def20 defines Rule2 FOMODEL4:def_20_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule2 Seqts iff ( seqt `1 is empty &amp; ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t ) );

:: deftheorem Def21 defines Rule3a FOMODEL4:def_21_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule3a Seqts iff ex t, t1, t2 being termal string of S ex x being set st
( x in Seqts &amp; seqt `1 = (x `1) \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} &amp; x `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t1 &amp; seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 ) );

:: deftheorem Def22 defines Rule3b FOMODEL4:def_22_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule3b Seqts iff ex t1, t2 being termal string of S st
( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} &amp; seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 ) );

:: deftheorem Def23 defines Rule3d FOMODEL4:def_23_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule3d Seqts iff ex s being low-compounding Element of S ex T, U being abs (ar b4) -element Element of (AllTermsOf S) * st
( s is operational &amp; seqt `1 =  {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  &amp; seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) );

:: deftheorem Def24 defines Rule3e FOMODEL4:def_24_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule3e Seqts iff ex s being relational Element of S ex T, U being abs (ar b4) -element Element of (AllTermsOf S) * st
( seqt `1 = {(s -compound T)} \/  {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  &amp; seqt `2 = s -compound U ) );

:: deftheorem Def25 defines Rule4 FOMODEL4:def_25_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule4 Seqts iff ex l being literal Element of S ex phi being wff string of S ex t being termal string of S st
( seqt `1 = {((l,t) SubstIn phi)} &amp; seqt `2 = <*l*> ^ phi ) );

:: deftheorem Def26 defines Rule5 FOMODEL4:def_26_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule5 Seqts iff ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st
( seqt `1 = x \/ {(<*v1*> ^ p)} &amp; v2 is (x \/ {p}) \/ {(seqt `2)} -absent &amp; [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts ) );

:: deftheorem Def27 defines Rule6 FOMODEL4:def_27_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule6 Seqts iff ex y1, y2 being set ex phi1, phi2 being wff string of S st
( y1 in Seqts &amp; y2 in Seqts &amp; y1 `1 = y2 `1 &amp; y2 `1 = seqt `1 &amp; y1 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi1 &amp; y2 `2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi2 &amp; seqt `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ) );

:: deftheorem Def28 defines Rule7 FOMODEL4:def_28_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule7 Seqts iff ex y being set ex phi1, phi2 being wff string of S st
( y in Seqts &amp; y `1 = seqt `1 &amp; y `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; seqt `2 = (<*(TheNorSymbOf S)*> ^ phi2) ^ phi1 ) );

:: deftheorem Def29 defines Rule8 FOMODEL4:def_29_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule8 Seqts iff ex y1, y2 being set ex phi, phi1, phi2 being wff string of S st
( y1 in Seqts &amp; y2 in Seqts &amp; y1 `1 = y2 `1 &amp; y1 `2 = phi1 &amp; y2 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; {phi} \/ (seqt `1) = y1 `1 &amp; seqt `2 = (<*(TheNorSymbOf S)*> ^ phi) ^ phi ) );

:: deftheorem Def30 defines Rule9 FOMODEL4:def_30_:_
 for Seqts being set
for S being Language
for seqt being b2 -null set holds
( seqt Rule9 Seqts iff ex y being set ex phi being wff string of S st
( y in Seqts &amp; seqt `2 = phi &amp; y `1 = seqt `1 &amp; y `2 = xnot (xnot phi) ) );

definition
let S be Language;
func P#0 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def31: :: FOMODEL4:def 31
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule0 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule0 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule0 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule0 Seqts ) ) holds
b1 = b2
proofend;
func P#1 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def32: :: FOMODEL4:def 32
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule1 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule1 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule1 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule1 Seqts ) ) holds
b1 = b2
proofend;
func P#2 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def33: :: FOMODEL4:def 33
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule2 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule2 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule2 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule2 Seqts ) ) holds
b1 = b2
proofend;
func P#3a S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def34: :: FOMODEL4:def 34
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3a Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3a Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3a Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3a Seqts ) ) holds
b1 = b2
proofend;
func P#3b S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def35: :: FOMODEL4:def 35
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3b Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3b Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3b Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3b Seqts ) ) holds
b1 = b2
proofend;
func P#3d S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def36: :: FOMODEL4:def 36
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3d Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3d Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3d Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3d Seqts ) ) holds
b1 = b2
proofend;
func P#3e S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def37: :: FOMODEL4:def 37
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3e Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3e Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule3e Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3e Seqts ) ) holds
b1 = b2
proofend;
func P#4 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def38: :: FOMODEL4:def 38
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule4 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule4 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule4 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule4 Seqts ) ) holds
b1 = b2
proofend;
func P#5 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def39: :: FOMODEL4:def 39
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule5 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule5 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule5 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule5 Seqts ) ) holds
b1 = b2
proofend;
func P#6 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def40: :: FOMODEL4:def 40
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule6 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule6 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule6 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule6 Seqts ) ) holds
b1 = b2
proofend;
func P#7 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def41: :: FOMODEL4:def 41
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule7 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule7 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule7 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule7 Seqts ) ) holds
b1 = b2
proofend;
func P#8 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def42: :: FOMODEL4:def 42
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule8 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule8 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule8 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule8 Seqts ) ) holds
b1 = b2
proofend;
func P#9 S ->  Relation of (bool (S -sequents)),(S -sequents) means :Def43: :: FOMODEL4:def 43
 for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule9 Seqts );
existence
 ex b1 being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule9 Seqts )
proofend;
uniqueness
 for b1, b2 being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b1 iff seqt Rule9 Seqts ) ) &amp; ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule9 Seqts ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def31 defines P#0 FOMODEL4:def_31_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#0 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule0 Seqts ) );

:: deftheorem Def32 defines P#1 FOMODEL4:def_32_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#1 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule1 Seqts ) );

:: deftheorem Def33 defines P#2 FOMODEL4:def_33_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#2 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule2 Seqts ) );

:: deftheorem Def34 defines P#3a FOMODEL4:def_34_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#3a S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3a Seqts ) );

:: deftheorem Def35 defines P#3b FOMODEL4:def_35_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#3b S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3b Seqts ) );

:: deftheorem Def36 defines P#3d FOMODEL4:def_36_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#3d S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3d Seqts ) );

:: deftheorem Def37 defines P#3e FOMODEL4:def_37_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#3e S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule3e Seqts ) );

:: deftheorem Def38 defines P#4 FOMODEL4:def_38_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#4 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule4 Seqts ) );

:: deftheorem Def39 defines P#5 FOMODEL4:def_39_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#5 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule5 Seqts ) );

:: deftheorem Def40 defines P#6 FOMODEL4:def_40_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#6 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule6 Seqts ) );

:: deftheorem Def41 defines P#7 FOMODEL4:def_41_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#7 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule7 Seqts ) );

:: deftheorem Def42 defines P#8 FOMODEL4:def_42_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#8 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule8 Seqts ) );

:: deftheorem Def43 defines P#9 FOMODEL4:def_43_:_
 for S being Language
for b2 being Relation of (bool (S -sequents)),(S -sequents) holds
( b2 = P#9 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b2 iff seqt Rule9 Seqts ) );

definition
let S be Language;
let R be Relation of (bool (S -sequents)),(S -sequents);
func FuncRule R ->  Rule of S means :Def44: :: FOMODEL4:def 44
 for inseqs being set st inseqs in bool (S -sequents) holds
it . inseqs =  {  x where x is Element of S -sequents : [inseqs,x] in R  }  ;
existence
 ex b1 being Rule of S st
for inseqs being set st inseqs in bool (S -sequents) holds
b1 . inseqs =  {  x where x is Element of S -sequents : [inseqs,x] in R  }
proofend;
uniqueness
 for b1, b2 being Rule of S st ( for inseqs being set st inseqs in bool (S -sequents) holds
b1 . inseqs =  {  x where x is Element of S -sequents : [inseqs,x] in R  }  ) &amp; ( for inseqs being set st inseqs in bool (S -sequents) holds
b2 . inseqs =  {  x where x is Element of S -sequents : [inseqs,x] in R  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def44 defines FuncRule FOMODEL4:def_44_:_
 for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents)
for b3 being Rule of S holds
( b3 = FuncRule R iff for inseqs being set st inseqs in bool (S -sequents) holds
b3 . inseqs =  {  x where x is Element of S -sequents : [inseqs,x] in R  }  );

Lm26:  for S being Language
for Seqts being Subset of (S -sequents)
for seqt being Element of S -sequents
for R being Relation of (bool (S -sequents)),(S -sequents) st [Seqts,seqt] in R holds
seqt in (FuncRule R) . Seqts
proofend;

Lm27:  for S being Language
for SQ being b1 -sequents-like set
for Sq being b1 -sequent-like set
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq is 1,SQ,{(FuncRule R)} -derivable
proofend;

Lm28:  for y being set
for S being Language
for SQ being b2 -sequents-like set
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . SQ iff ( y in S -sequents &amp; [SQ,y] in R ) )
proofend;

Lm29:  for y, X being set
for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . X iff ( y in S -sequents &amp; [X,y] in R ) )
proofend;

definition
let S be Language;
func R#0 S ->  Rule of S equals :: FOMODEL4:def 45
 FuncRule (P#0 S);
coherence
 FuncRule (P#0 S) is Rule of S ;
func R#1 S ->  Rule of S equals :: FOMODEL4:def 46
 FuncRule (P#1 S);
coherence
 FuncRule (P#1 S) is Rule of S ;
func R#2 S ->  Rule of S equals :: FOMODEL4:def 47
 FuncRule (P#2 S);
coherence
 FuncRule (P#2 S) is Rule of S ;
func R#3a S ->  Rule of S equals :: FOMODEL4:def 48
 FuncRule (P#3a S);
coherence
 FuncRule (P#3a S) is Rule of S ;
func R#3b S ->  Rule of S equals :: FOMODEL4:def 49
 FuncRule (P#3b S);
coherence
 FuncRule (P#3b S) is Rule of S ;
func R#3d S ->  Rule of S equals :: FOMODEL4:def 50
 FuncRule (P#3d S);
coherence
 FuncRule (P#3d S) is Rule of S ;
func R#3e S ->  Rule of S equals :: FOMODEL4:def 51
 FuncRule (P#3e S);
coherence
 FuncRule (P#3e S) is Rule of S ;
func R#4 S ->  Rule of S equals :: FOMODEL4:def 52
 FuncRule (P#4 S);
coherence
 FuncRule (P#4 S) is Rule of S ;
func R#5 S ->  Rule of S equals :: FOMODEL4:def 53
 FuncRule (P#5 S);
coherence
 FuncRule (P#5 S) is Rule of S ;
func R#6 S ->  Rule of S equals :: FOMODEL4:def 54
 FuncRule (P#6 S);
coherence
 FuncRule (P#6 S) is Rule of S ;
func R#7 S ->  Rule of S equals :: FOMODEL4:def 55
 FuncRule (P#7 S);
coherence
 FuncRule (P#7 S) is Rule of S ;
func R#8 S ->  Rule of S equals :: FOMODEL4:def 56
 FuncRule (P#8 S);
coherence
 FuncRule (P#8 S) is Rule of S ;
func R#9 S ->  Rule of S equals :: FOMODEL4:def 57
 FuncRule (P#9 S);
coherence
 FuncRule (P#9 S) is Rule of S ;
end;

:: deftheorem  defines R#0 FOMODEL4:def_45_:_
 for S being Language holds R#0 S = FuncRule (P#0 S);

:: deftheorem  defines R#1 FOMODEL4:def_46_:_
 for S being Language holds R#1 S = FuncRule (P#1 S);

:: deftheorem  defines R#2 FOMODEL4:def_47_:_
 for S being Language holds R#2 S = FuncRule (P#2 S);

:: deftheorem  defines R#3a FOMODEL4:def_48_:_
 for S being Language holds R#3a S = FuncRule (P#3a S);

:: deftheorem  defines R#3b FOMODEL4:def_49_:_
 for S being Language holds R#3b S = FuncRule (P#3b S);

:: deftheorem  defines R#3d FOMODEL4:def_50_:_
 for S being Language holds R#3d S = FuncRule (P#3d S);

:: deftheorem  defines R#3e FOMODEL4:def_51_:_
 for S being Language holds R#3e S = FuncRule (P#3e S);

:: deftheorem  defines R#4 FOMODEL4:def_52_:_
 for S being Language holds R#4 S = FuncRule (P#4 S);

:: deftheorem  defines R#5 FOMODEL4:def_53_:_
 for S being Language holds R#5 S = FuncRule (P#5 S);

:: deftheorem  defines R#6 FOMODEL4:def_54_:_
 for S being Language holds R#6 S = FuncRule (P#6 S);

:: deftheorem  defines R#7 FOMODEL4:def_55_:_
 for S being Language holds R#7 S = FuncRule (P#7 S);

:: deftheorem  defines R#8 FOMODEL4:def_56_:_
 for S being Language holds R#8 S = FuncRule (P#8 S);

:: deftheorem  defines R#9 FOMODEL4:def_57_:_
 for S being Language holds R#9 S = FuncRule (P#9 S);

registration
let S be Language;
let t be termal string of S;
cluster{[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} -> {(R#2 S)} -derivable for set ;
coherence
 for b1 being set st b1 = {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} holds
b1 is {(R#2 S)} -derivable
proofend;
end;

registration
let S be Language;
cluster R#2 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#2 S holds
b1 is isotone
proofend;
end;

Lm30:  for X being set
for S being Language
for D being RuleSet of S st {(R#2 S)} c= D holds
(X,D) -termEq is total
proofend;

registration
let S be Language;
cluster R#3b S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3b S holds
b1 is isotone
proofend;
end;

Lm31:  for X being set
for S being Language
for D being RuleSet of S st {(R#3b S)} c= D &amp; X is D -expanded holds
(X,D) -termEq is symmetric
proofend;

registration
let S be Language;
let t, t1, t2 be termal string of S;
let premises be finite Subset of (AllFormulasOf S);
cluster[(premises \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)}),((<*(TheEqSymbOf S)*> ^ t) ^ t2)] -> 1,{[premises,((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R#3a S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(premises \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)}),((<*(TheEqSymbOf S)*> ^ t) ^ t2)] holds
b1 is 1,{[premises,((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R#3a S)} -derivable
proofend;
end;

registration
let S be Language;
let t, t1, t2 be termal string of S;
let phi be wff string of S;
cluster[{phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)},((<*(TheEqSymbOf S)*> ^ t) ^ t2)] -> 1,{[{phi},((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R#3a S)} -derivable for set ;
coherence
 for b1 being set st b1 = [{phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)},((<*(TheEqSymbOf S)*> ^ t) ^ t2)] holds
b1 is 1,{[{phi},((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R#3a S)} -derivable
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
let Phi be finite Subset of (AllFormulasOf S);
cluster[(Phi \/ {phi}),phi] -> 1, {} ,{(R#0 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(Phi \/ {phi}),phi] holds
b1 is 1, {} ,{(R#0 S)} -derivable
proofend;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster[{phi1,phi2},phi1] -> 1, {} ,{(R#0 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [{phi1,phi2},phi1] holds
b1 is 1, {} ,{(R#0 S)} -derivable
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
cluster[{phi},phi] -> 1, {} ,{(R#0 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [{phi},phi] holds
b1 is 1, {} ,{(R#0 S)} -derivable
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
cluster{[{phi},phi]} ->  {} ,{(R#0 S)} -derivable for set ;
coherence
 for b1 being set st b1 = {[{phi},phi]} holds
b1 is {} ,{(R#0 S)} -derivable by Lm12;
end;

registration
let S be Language;
cluster R#0 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#0 S holds
b1 is isotone
proofend;
cluster R#3a S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3a S holds
b1 is isotone
proofend;
cluster R#3d S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3d S holds
b1 is isotone
proofend;
cluster R#3e S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3e S holds
b1 is isotone
proofend;
let K1, K2 be isotone RuleSet of S;
clusterK1 \/ K2 ->  isotone for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = K1 \/ K2 holds
b1 is isotone
proofend;
end;

Lm32:  for X being set
for S being Language
for D being RuleSet of S st {(R#0 S)} \/ {(R#3a S)} c= D &amp; X is D -expanded holds
(X,D) -termEq is transitive
proofend;

Lm33:  for X being set
for S being Language
for D being RuleSet of S st {(R#0 S),(R#3a S)} c= D &amp; {(R#2 S),(R#3b S)} c= D &amp; X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
proofend;

registration
let S be Language;
let t1, t2 be termal string of S;
cluster(<*(TheEqSymbOf S)*> ^ t1) ^ t2 ->  0 -wff for string of S;
coherence
 for b1 being string of S st b1 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 holds
b1 is 0 -wff by Lm2;
end;

definition
let S be Language;
let m be non zero Nat;
let T, U be m -element Element of (AllTermsOf S) * ;
func PairWiseEq (T,U) ->  set  equals :: FOMODEL4:def 58
 {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg m, TT, UU is Function of (Seg m),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  ;
coherence
  {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg m, TT, UU is Function of (Seg m),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  is set ;
end;

:: deftheorem  defines PairWiseEq FOMODEL4:def_58_:_
 for S being Language
for m being non zero Nat
for T, U being b2 -element Element of (AllTermsOf S) * holds PairWiseEq (T,U) =  {  ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg m, TT, UU is Function of (Seg m),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T &amp; UU = U )  }  ;

definition
let S be Language;
let m be non zero Nat;
let T1, T2 be m -element Element of (AllTermsOf S) * ;
:: original:PairWiseEq
redefine func PairWiseEq (T1,T2) ->  Subset of (AllFormulasOf S);
coherence
 PairWiseEq (T1,T2) is Subset of (AllFormulasOf S)
proofend;
end;

registration
let S be Language;
let m be non zero Nat;
let T, U be m -element Element of (AllTermsOf S) * ;
cluster PairWiseEq (T,U) ->  finite ;
coherence
 PairWiseEq (T,U) is finite
proofend;
end;

Lm34:  for S being Language
for s being low-compounding Element of S
for T, U being abs (ar b2) -element Element of (AllTermsOf S) * st s is termal holds
{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable
proofend;

Lm35:  for S being Language
for s being relational Element of S
for T1, T2 being abs (ar b2) -element Element of (AllTermsOf S) * holds {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable
proofend;

registration
let S be Language;
let s be relational Element of S;
let T1, T2 be abs (ar s) -element Element of (AllTermsOf S) * ;
cluster{[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} ->  {} ,{(R#3e S)} -derivable ;
coherence
 {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable by Lm35;
end;

Lm36:  for X, x1, x2 being set
for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st X is D -expanded &amp; [x1,x2] in (abs (ar s)) -placesOf ((X,D) -termEq) holds
ex T, U being abs (ar b6) -element Element of (AllTermsOf S) * st
( T = x1 &amp; U = x2 &amp; PairWiseEq (T,U) c= X )
proofend;

Lm37:  for X being set
for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st {(R#3d S)} c= D &amp; X is D -expanded &amp; s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
proofend;

Lm38:  for X, x1, x2 being set
for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R#3e S)} c= D &amp; X is D -expanded &amp; [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) &amp; (r -compound) . x1 in X holds
(r -compound) . x2 in X
proofend;

Lm39:  for X, x1, x2 being set
for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} &amp; {(R#3b S)} /\ D = {(R#3b S)} &amp; D /\ {(R#3e S)} = {(R#3e S)} &amp; X is D -expanded &amp; [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) holds
( (r -compound) . x1 in X iff (r -compound) . x2 in X )
proofend;

Lm40:  for U being non empty set
for Y being set
for x, y being Element of U holds
not ( ( x in Y implies y in Y ) &amp; ( y in Y implies x in Y ) &amp; not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN )
proofend;

Lm41:  for X being set
for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} &amp; {(R#3b S)} /\ D = {(R#3b S)} &amp; D /\ {(R#3e S)} = {(R#3e S)} &amp; X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting
proofend;

Lm42:  for U being non empty set
for X, x being set
for R being total reflexive Relation of U
for f being Function of X,U st x in X holds
f is {[x,x]},R -respecting
proofend;

Lm43:  for U being non empty set
for S being Language
for l being literal Element of S
for E being total reflexive Relation of U
for f being Interpreter of l,U holds f is E -respecting
proofend;

Lm44:  for X being set
for S being Language
for l being literal Element of S
for D being RuleSet of S st {(R#0 S),(R#3a S)} c= D &amp; {(R#2 S),(R#3b S)} c= D &amp; X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
proofend;

Lm45:  for X being set
for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R#0 S),(R#3a S)} c= D &amp; D /\ {(R#3d S)} = {(R#3d S)} &amp; {(R#2 S)} /\ D = {(R#2 S)} &amp; {(R#3b S)} /\ D = {(R#3b S)} &amp; D /\ {(R#3e S)} = {(R#3e S)} &amp; X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
proofend;

definition
let m be Nat;
let S be Language;
let D be RuleSet of S;
attrD is m -ranked  means :Def59: :: FOMODEL4:def 59
( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D ) if m = 0
( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D ) if m = 1
( R#0 S in D &amp; R#1 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D &amp; R#4 S in D &amp; R#5 S in D &amp; R#6 S in D &amp; R#7 S in D &amp; R#8 S in D ) if m = 2
otherwise D = {} ;
consistency
 ( ( m = 0 &amp; m = 1 implies ( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D iff ( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D ) ) ) &amp; ( m = 0 &amp; m = 2 implies ( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D iff ( R#0 S in D &amp; R#1 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D &amp; R#4 S in D &amp; R#5 S in D &amp; R#6 S in D &amp; R#7 S in D &amp; R#8 S in D ) ) ) &amp; ( m = 1 &amp; m = 2 implies ( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D iff ( R#0 S in D &amp; R#1 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D &amp; R#4 S in D &amp; R#5 S in D &amp; R#6 S in D &amp; R#7 S in D &amp; R#8 S in D ) ) ) ) ;
end;

:: deftheorem Def59 defines -ranked FOMODEL4:def_59_:_
 for m being Nat
for S being Language
for D being RuleSet of S holds
( ( m = 0 implies ( D is m -ranked iff ( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D ) ) ) &amp; ( m = 1 implies ( D is m -ranked iff ( R#0 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D ) ) ) &amp; ( m = 2 implies ( D is m -ranked iff ( R#0 S in D &amp; R#1 S in D &amp; R#2 S in D &amp; R#3a S in D &amp; R#3b S in D &amp; R#3d S in D &amp; R#3e S in D &amp; R#4 S in D &amp; R#5 S in D &amp; R#6 S in D &amp; R#7 S in D &amp; R#8 S in D ) ) ) &amp; ( not m = 0 &amp; not m = 1 &amp; not m = 2 implies ( D is m -ranked iff D = {} ) ) );

registration
let S be Language;
cluster1 -ranked  ->  0 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
coherence
 for b1 being RuleSet of S st b1 is 1 -ranked holds
b1 is 0 -ranked
proofend;
cluster2 -ranked  -> 1 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
coherence
 for b1 being RuleSet of S st b1 is 2 -ranked holds
b1 is 1 -ranked
proofend;
end;

definition
let S be Language;
funcS -rules  ->  RuleSet of S equals :: FOMODEL4:def 60
{(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};
coherence
 {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} is RuleSet of S ;
end;

:: deftheorem  defines -rules FOMODEL4:def_60_:_
 for S being Language holds S -rules = {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};

registration
let S be Language;
clusterS -rules  -> 2 -ranked for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = S -rules holds
b1 is 2 -ranked
proofend;
end;

registration
let S be Language;
cluster functional 2 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being RuleSet of S st b1 is 2 -ranked
proofend;
end;

registration
let S be Language;
cluster functional 1 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being RuleSet of S st b1 is 1 -ranked
proofend;
end;

registration
let S be Language;
cluster functional 0 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being RuleSet of S st b1 is 0 -ranked
proofend;
end;

Lm46:  for X being set
for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st D is 1 -ranked &amp; X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
proofend;

registration
let S be Language;
let D be 1 -ranked RuleSet of S;
let X be D -expanded set ;
let a be ofAtomicFormula Element of S;
clusterX -freeInterpreter a -> (X,D) -termEq -respecting for Interpreter of a, AllTermsOf S;
coherence
 for b1 being Interpreter of a, AllTermsOf S st b1 = X -freeInterpreter a holds
b1 is (X,D) -termEq -respecting by Lm46;
end;

Lm47:  for X being set
for S being Language
for D being RuleSet of S st D is 0 -ranked &amp; X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)
proofend;

registration
let S be Language;
let D be 0 -ranked RuleSet of S;
let X be D -expanded set ;
cluster(X,D) -termEq  ->  total symmetric transitive for Relation of (AllTermsOf S);
coherence
 for b1 being Relation of (AllTermsOf S) st b1 = (X,D) -termEq holds
( b1 is total &amp; b1 is symmetric &amp; b1 is transitive ) by Lm47;
end;

registration
let S be Language;
cluster functional 0 -ranked 1 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being 0 -ranked RuleSet of S st b1 is 1 -ranked
proofend;
end;

theorem :: FOMODEL4:1
for Y, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) &amp; Y is X,D1 -derivable holds
Y is X,D2 -derivable by Lm18;

registration
let S be Language;
let Sq be S -sequent-like set ;
cluster{Sq} -> S -sequents-like ;
coherence
 {Sq} is S -sequents-like
proofend;
end;

registration
let S be Language;
let SQ1, SQ2 be S -sequents-like set ;
clusterSQ1 \/ SQ2 -> S -sequents-like for set ;
coherence
 for b1 being set st b1 = SQ1 \/ SQ2 holds
b1 is S -sequents-like
proofend;
end;

registration
let S be Language;
let x, y be S -sequent-like set ;
cluster{x,y} -> S -sequents-like for set ;
coherence
 for b1 being set st b1 = {x,y} holds
b1 is S -sequents-like
proofend;
end;

Lm48:  for m, n being Nat
for x, y, z being set
for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b6 -sequents-like set st D1 \/ D2 is isotone &amp; (D1 \/ D2) \/ D3 is isotone &amp; x is m,SQ1,D1 -derivable &amp; y is m,SQ2,D2 -derivable &amp; z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable
proofend;

Lm49:  for x, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D1 is isotone or D2 is isotone ) &amp; x is X,D1 -provable holds
x is X,D2 -provable
proofend;

Lm50:  for x, X being set
for S being Language
for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable
proofend;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster[{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] -> 1,{[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]},{(R#6 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] holds
b1 is 1,{[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]},{(R#6 S)} -derivable
proofend;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster[{phi1,phi2},phi2] -> 1, {} ,{(R#0 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [{phi1,phi2},phi2] holds
b1 is 1, {} ,{(R#0 S)} -derivable
proofend;
end;

theorem Th2: :: FOMODEL4:2
for S being Language
for SQ being b1 -sequents-like set
for Sq being b1 -sequent-like set
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq in (FuncRule R) . SQ
proofend;

theorem :: FOMODEL4:3
for x, X being set
for S being Language
for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable by Lm50;

definition
let S be Language;
let D be RuleSet of S;
let X be set ;
redefine attr X is D -expanded  means :Def61: :: FOMODEL4:def 61
 for x being set st x is X,D -provable holds
x in X;
compatibility
 ( X is D -expanded iff for x being set st x is X,D -provable holds
x in X )
proofend;
end;

:: deftheorem Def61 defines -expanded FOMODEL4:def_61_:_
 for S being Language
for D being RuleSet of S
for X being set holds
( X is D -expanded iff for x being set st x is X,D -provable holds
x in X );

theorem Th4: :: FOMODEL4:4
for X being set
for S being Language
for phi being wff string of S st phi in X holds
phi is X,{(R#0 S)} -provable
proofend;

theorem :: FOMODEL4:5
for m, n being Nat
for x, y, z being set
for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b6 -sequents-like set st D1 \/ D2 is isotone &amp; (D1 \/ D2) \/ D3 is isotone &amp; x is m,SQ1,D1 -derivable &amp; y is m,SQ2,D2 -derivable &amp; z is n,{x,y},D3 -derivable holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable by Lm48;

theorem :: FOMODEL4:6
for m, n being Nat
for y, X, z being set
for S being Language
for D1, D2 being RuleSet of S st D1 is isotone &amp; D1 \/ D2 is isotone &amp; y is m,X,D1 -derivable &amp; z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable by Lm21;

theorem :: FOMODEL4:7
for m being Nat
for x, X being set
for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable by Lm12;

registration
let S be Language;
cluster R#6 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#6 S holds
b1 is isotone
proofend;
end;

theorem :: FOMODEL4:8
for x, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D1 is isotone or D2 is isotone ) &amp; x is X,D1 -provable holds
x is X,D2 -provable by Lm49;

theorem :: FOMODEL4:9
for X, Y, x being set
for S being Language
for D being RuleSet of S st X c= Y &amp; x is X,D -provable holds
x is Y,D -provable ;

registration
let S be Language;
cluster R#8 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#8 S holds
b1 is isotone
proofend;
end;

registration
let S be Language;
cluster R#1 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#1 S holds
b1 is isotone
proofend;
end;

theorem :: FOMODEL4:10
for y being set
for S being Language
for D being RuleSet of S
for SQ being b2 -sequents-like set st {y} is SQ,D -derivable holds
ex mm being Element of NAT st y is mm,SQ,D -derivable
proofend;

registration
let S be Language;
let D be RuleSet of S;
let X be set ;
clusterX,D -derivable  -> S -sequents-like for set ;
coherence
 for b1 being set st b1 is X,D -derivable holds
b1 is S -sequents-like
proofend;
end;

definition
let S be Language;
let D be RuleSet of S;
let X, x be set ;
redefine attr x is X,D -provable  means :Def62: :: FOMODEL4:def 62
 ex H being set ex m being Nat st
( H c= X &amp; [H,x] is m, {} ,D -derivable );
compatibility
 ( x is X,D -provable iff ex H being set ex m being Nat st
( H c= X &amp; [H,x] is m, {} ,D -derivable ) )
proofend;
end;

:: deftheorem Def62 defines -provable FOMODEL4:def_62_:_
 for S being Language
for D being RuleSet of S
for X, x being set holds
( x is X,D -provable iff ex H being set ex m being Nat st
( H c= X &amp; [H,x] is m, {} ,D -derivable ) );

theorem Th11: :: FOMODEL4:11
for m being Nat
for x, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 &amp; ( D2 is isotone or D1 is isotone ) &amp; x is m,X,D1 -derivable holds
x is m,X,D2 -derivable
proofend;

registration
let S be Language;
cluster R#7 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#7 S holds
b1 is isotone
proofend;
end;

theorem :: FOMODEL4:12
for x, X being set
for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S by Lm24;

registration
let S be Language;
let D1 be 0 -ranked 1 -ranked RuleSet of S;
let X be D1 -expanded set ;
cluster(S,X) -freeInterpreter  -> S, AllTermsOf S -interpreter-like (X,D1) -termEq -respecting for S, AllTermsOf S -interpreter-like Function;
coherence
 for b1 being S, AllTermsOf S -interpreter-like Function st b1 = (S,X) -freeInterpreter holds
b1 is (X,D1) -termEq -respecting
proofend;
end;

definition
let S be Language;
let D be 0 -ranked RuleSet of S;
let X be D -expanded set ;
funcD Henkin X ->  Function equals :: FOMODEL4:def 63
((S,X) -freeInterpreter) quotient ((X,D) -termEq);
coherence
 ((S,X) -freeInterpreter) quotient ((X,D) -termEq) is Function ;
end;

:: deftheorem  defines Henkin FOMODEL4:def_63_:_
 for S being Language
for D being 0 -ranked RuleSet of S
for X being b2 -expanded set holds D Henkin X = ((S,X) -freeInterpreter) quotient ((X,D) -termEq);

registration
let S be Language;
let D be 0 -ranked RuleSet of S;
let X be D -expanded set ;
clusterD Henkin X ->  OwnSymbolsOf S -defined ;
coherence
 D Henkin X is OwnSymbolsOf S -defined ;
end;

registration
let S be Language;
let D1 be 0 -ranked 1 -ranked RuleSet of S;
let X be D1 -expanded set ;
clusterD1 Henkin X -> S, Class ((X,D1) -termEq) -interpreter-like for Function;
coherence
 for b1 being Function st b1 = D1 Henkin X holds
b1 is S, Class ((X,D1) -termEq) -interpreter-like ;
end;

definition
let S be Language;
let D1 be 0 -ranked 1 -ranked RuleSet of S;
let X be D1 -expanded set ;
:: original:Henkin
redefine funcD1 Henkin X ->  Element of (Class ((X,D1) -termEq)) -InterpretersOf S;
coherence
 D1 Henkin X is Element of (Class ((X,D1) -termEq)) -InterpretersOf S
proofend;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster(<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> {(xnot phi1),(xnot phi2)},{(R#0 S)} \/ {(R#6 S)} -provable for set ;
coherence
 for b1 being set st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is {(xnot phi1),(xnot phi2)},{(R#0 S)} \/ {(R#6 S)} -provable
proofend;
end;

registration
let S be Language;
cluster 0 -ranked  ->  non empty 0 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
coherence
 for b1 being 0 -ranked RuleSet of S holds not b1 is empty by Def59;
end;

definition
let S be Language;
let x be set ;
attrx is S -premises-like  means :Def64: :: FOMODEL4:def 64
( x c= AllFormulasOf S &amp; x is finite );
end;

:: deftheorem Def64 defines -premises-like FOMODEL4:def_64_:_
 for S being Language
for x being set holds
( x is S -premises-like iff ( x c= AllFormulasOf S &amp; x is finite ) );

registration
let S be Language;
clusterS -premises-like  ->  finite for set ;
coherence
 for b1 being set st b1 is S -premises-like holds
b1 is finite by Def64;
end;

registration
let S be Language;
let phi be wff string of S;
cluster{phi} -> S -premises-like for set ;
coherence
 for b1 being set st b1 = {phi} holds
b1 is S -premises-like
proofend;
end;

registration
let S be Language;
let e be empty set ;
clustere null S -> S -premises-like for set ;
coherence
 for b1 being set st b1 = e null S holds
b1 is S -premises-like
proofend;
end;

registration
let X be set ;
let S be Language;
clusterS -premises-like for Element of bool X;
existence
 ex b1 being Subset of X st b1 is S -premises-like
proofend;
end;

registration
let S be Language;
clusterS -premises-like for set ;
existence
 ex b1 being set st b1 is S -premises-like
proofend;
end;

registration
let S be Language;
let X be S -premises-like set ;
cluster  -> S -premises-like for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is S -premises-like
proofend;
end;

definition
let S be Language;
let H2, H1 be S -premises-like set ;
:: original:null
redefine funcH1 null H2 ->  Subset of (AllFormulasOf S);
coherence
 H1 null H2 is Subset of (AllFormulasOf S) by Def64;
end;

registration
let S be Language;
let H be S -premises-like set ;
let x be set ;
clusterH null x -> S -premises-like ;
coherence
 H null x is S -premises-like ;
end;

registration
let S be Language;
let H1, H2 be S -premises-like set ;
clusterH1 \/ H2 -> S -premises-like for set ;
coherence
 for b1 being set st b1 = H1 \/ H2 holds
b1 is S -premises-like
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi be wff string of S;
cluster[H,phi] -> S -sequent-like ;
coherence
 [H,phi] is S -sequent-like
proofend;
end;

registration
let S be Language;
let H1, H2 be S -premises-like set ;
let phi be wff string of S;
cluster[(H1 \/ H2),phi] -> 1,{[H1,phi]},{(R#1 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(H1 \/ H2),phi] holds
b1 is 1,{[H1,phi]},{(R#1 S)} -derivable
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi, phi1, phi2 be wff string of S;
cluster[(H null (phi1 ^ phi2)),(xnot phi)] -> 1,{[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#8 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(H null (phi1 ^ phi2)),(xnot phi)] holds
b1 is 1,{[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#8 S)} -derivable
proofend;
end;

registration
let S be Language;
cluster{} null S -> S -sequents-like for set ;
coherence
 for b1 being set st b1 = {} null S holds
b1 is S -sequents-like
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi be wff string of S;
cluster[(H \/ {phi}),phi] -> 1, {} ,{(R#0 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(H \/ {phi}),phi] holds
b1 is 1, {} ,{(R#0 S)} -derivable
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi1, phi2 be wff string of S;
cluster[(H null phi2),(xnot phi1)] -> 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(H null phi2),(xnot phi1)] holds
b1 is 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi1, phi2 be wff string of S;
cluster[H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] -> 1,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#7 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] holds
b1 is 1,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#7 S)} -derivable
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi1, phi2 be wff string of S;
cluster[(H null phi1),(xnot phi2)] -> 3,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},(({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) \/ {(R#7 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [(H null phi1),(xnot phi2)] holds
b1 is 3,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},(({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) \/ {(R#7 S)} -derivable
proofend;
end;

registration
let S be Language;
let Sq be S -sequent-like set ;
clusterSq `1  -> S -premises-like for set ;
coherence
 for b1 being set st b1 = Sq `1 holds
b1 is S -premises-like
proofend;
end;

definition
let S be Language;
let X be set ;
let D be RuleSet of S;
:: original:null
redefine funcD null X ->  RuleSet of S;
coherence
 D null X is RuleSet of S ;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
let l1 be literal Element of S;
let H be S -premises-like set ;
let l2 be literal (H \/ {phi1}) \/ {phi2} -absent Element of S;
cluster[((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] -> 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R#5 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] holds
b1 is 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R#5 S)} -derivable
proofend;
end;

definition
let S be Language;
let D be RuleSet of S;
let X be set ;
attrX is D -inconsistent  means :Def65: :: FOMODEL4:def 65
 ex phi1, phi2 being wff string of S st
( phi1 is X,D -provable &amp; (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable );
end;

:: deftheorem Def65 defines -inconsistent FOMODEL4:def_65_:_
 for S being Language
for D being RuleSet of S
for X being set holds
( X is D -inconsistent iff ex phi1, phi2 being wff string of S st
( phi1 is X,D -provable &amp; (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) );

registration
let m1 be non zero Nat;
let S be Language;
let H1, H2 be S -premises-like set ;
let phi be wff string of S;
cluster[((H1 \/ H2) null m1),phi] -> m1,{[H1,phi]},{(R#1 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [((H1 \/ H2) null m1),phi] holds
b1 is m1,{[H1,phi]},{(R#1 S)} -derivable
proofend;
end;

registration
let S be Language;
cluster non empty functional isotone for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 not for b1 being isotone RuleSet of S holds b1 is empty
proofend;
end;

theorem Th13: :: FOMODEL4:13
for X being set
for S being Language
for phi being wff string of S
for D being RuleSet of S st X is D -inconsistent &amp; D is isotone &amp; R#1 S in D &amp; R#8 S in D holds
xnot phi is X,D -provable
proofend;

registration
let S be Language;
cluster R#5 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#5 S holds
b1 is isotone
proofend;
end;

registration
let S be Language;
let l be literal Element of S;
let t be termal string of S;
let phi be wff string of S;
cluster[{((l,t) SubstIn phi)},(<*l*> ^ phi)] -> 1, {} ,{(R#4 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] holds
b1 is 1, {} ,{(R#4 S)} -derivable
proofend;
end;

registration
let S be Language;
cluster R#4 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#4 S holds
b1 is isotone
proofend;
end;

Lm51:  for S being Language
for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b2 -expanded set
for phi being 0wff string of S holds
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )
proofend;

definition
let S be Language;
let X be set ;
attrX is S -witnessed  means :Def66: :: FOMODEL4:def 66
 for l1 being literal Element of S
for phi1 being wff string of S st <*l1*> ^ phi1 in X holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in X &amp; not l2 in rng phi1 );
end;

:: deftheorem Def66 defines -witnessed FOMODEL4:def_66_:_
 for S being Language
for X being set holds
( X is S -witnessed iff for l1 being literal Element of S
for phi1 being wff string of S st <*l1*> ^ phi1 in X holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in X &amp; not l2 in rng phi1 ) );

theorem Th14: :: FOMODEL4:14
for S being Language
for psi being wff string of S
for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b3 -expanded set st R#1 S in D1 &amp; R#4 S in D1 &amp; R#6 S in D1 &amp; R#7 S in D1 &amp; R#8 S in D1 &amp; X is S -mincover &amp; X is S -witnessed holds
( (D1 Henkin X) -TruthEval psi = 1 iff psi in X )
proofend;

notation
let S be Language;
let D be RuleSet of S;
let X be set ;
antonym D -consistent X for D -inconsistent ;
end;

theorem Th15: :: FOMODEL4:15
for Y being set
for S being Language
for D being RuleSet of S
for X being Subset of Y st X is D -inconsistent holds
Y is D -inconsistent
proofend;

definition
let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
func(D,phi) AddAsWitnessTo X ->  set  equals :Def67: :: FOMODEL4:def 67
X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} if ( X \/ {phi} is D -consistent &amp; (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} )
otherwise X;
consistency
 for b1 being set holds verum ;
coherence
 ( ( X \/ {phi} is D -consistent &amp; (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} implies X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} is set ) &amp; ( ( not X \/ {phi} is D -consistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies X is set ) ) ;
end;

:: deftheorem Def67 defines AddAsWitnessTo FOMODEL4:def_67_:_
 for S being Language
for D being RuleSet of S
for X being functional set
for phi being Element of ExFormulasOf S holds
( ( X \/ {phi} is D -consistent &amp; (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} implies (D,phi) AddAsWitnessTo X = X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} ) &amp; ( ( not X \/ {phi} is D -consistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies (D,phi) AddAsWitnessTo X = X ) );

registration
let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
clusterX \ ((D,phi) AddAsWitnessTo X) ->  empty for set ;
coherence
 for b1 being set st b1 = X \ ((D,phi) AddAsWitnessTo X) holds
b1 is empty
proofend;
end;

registration
let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
cluster((D,phi) AddAsWitnessTo X) \ X ->  trivial for set ;
coherence
 for b1 being set st b1 = ((D,phi) AddAsWitnessTo X) \ X holds
b1 is trivial
proofend;
end;

definition
let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
:: original:AddAsWitnessTo
redefine func(D,phi) AddAsWitnessTo X ->  Subset of (X \/ (AllFormulasOf S));
coherence
 (D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S))
proofend;
end;

definition
let S be Language;
let D be RuleSet of S;
attrD is Correct  means :Def68: :: FOMODEL4:def 68
 for phi being wff string of S
for X being set st phi is X,D -provable holds
for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1;
end;

:: deftheorem Def68 defines Correct FOMODEL4:def_68_:_
 for S being Language
for D being RuleSet of S holds
( D is Correct iff for phi being wff string of S
for X being set st phi is X,D -provable holds
for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1 );

Lm52:  for X being set
for S being Language
for phi being wff string of S
for D being RuleSet of S st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; X \/ {phi} is D -inconsistent holds
xnot phi is X,D -provable
proofend;

Lm53:  for X being set
for S being Language
for D being RuleSet of S holds
( X is D -consistent iff for Y being finite Subset of X holds Y is D -consistent )
proofend;

Lm54:  for X being set
for S being Language
for D being RuleSet of S st R#0 S in D &amp; X is S -covering &amp; X is D -consistent holds
( X is S -mincover &amp; X is D -expanded )
proofend;

Lm55:  for X being set
for S being Language
for phi being wff string of S
for D being RuleSet of S st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; phi is X,D -provable &amp; X is D -consistent holds
X \/ {phi} is D -consistent
proofend;

Lm56:  for U being non empty set
for X being set
for S being Language
for D being RuleSet of S
for I being Element of U -InterpretersOf S st D is Correct &amp; X is I -satisfied holds
X is D -consistent
proofend;

registration
let S be Language;
let t1, t2 be termal string of S;
cluster(SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> ->  empty for set ;
coherence
 for b1 being set st b1 = (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> holds
b1 is empty
proofend;
end;

Lm57:  for U being non empty set
for S being Language
for t1, t2 being termal string of S
for I being b2,b1 -interpreter-like Function holds
( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 )
proofend;

definition
let S be Language;
let R be Rule of S;
attrR is Correct  means :Def69: :: FOMODEL4:def 69
 for X being set st X is S -correct holds
R . X is S -correct ;
end;

:: deftheorem Def69 defines Correct FOMODEL4:def_69_:_
 for S being Language
for R being Rule of S holds
( R is Correct iff for X being set st X is S -correct holds
R . X is S -correct );

registration
let S be Language;
clusterS -sequent-like  -> S -null for set ;
coherence
 for b1 being set st b1 is S -sequent-like holds
b1 is S -null ;
end;

Lm58:  for S being Language holds R#0 S is Correct
proofend;

registration
let S be Language;
cluster R#0 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#0 S holds
b1 is Correct by Lm58;
end;

registration
let S be Language;
cluster Relation-like bool (S -sequents) -defined bool (S -sequents) -valued Function-like total quasi_total Correct for Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));
existence
 ex b1 being Rule of S st b1 is Correct
proofend;
end;

Lm59:  for S being Language holds R#1 S is Correct
proofend;

registration
let S be Language;
cluster R#1 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#1 S holds
b1 is Correct by Lm59;
end;

Lm60:  for S being Language holds R#2 S is Correct
proofend;

registration
let S be Language;
cluster R#2 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#2 S holds
b1 is Correct by Lm60;
end;

Lm61:  for S being Language holds R#3a S is Correct
proofend;

registration
let S be Language;
cluster R#3a S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3a S holds
b1 is Correct by Lm61;
end;

Lm62:  for S being Language holds R#3b S is Correct
proofend;

registration
let S be Language;
cluster R#3b S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3b S holds
b1 is Correct by Lm62;
end;

Lm63:  for S being Language holds R#3d S is Correct
proofend;

registration
let S be Language;
cluster R#3d S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3d S holds
b1 is Correct by Lm63;
end;

Lm64:  for S being Language holds R#3e S is Correct
proofend;

registration
let S be Language;
cluster R#3e S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#3e S holds
b1 is Correct by Lm64;
end;

Lm65:  for S being Language holds R#4 S is Correct
proofend;

registration
let S be Language;
cluster R#4 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#4 S holds
b1 is Correct by Lm65;
end;

Lm66:  for S being Language holds R#5 S is Correct
proofend;

registration
let S be Language;
cluster R#5 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#5 S holds
b1 is Correct by Lm66;
end;

Lm67:  for S being Language holds R#6 S is Correct
proofend;

registration
let S be Language;
cluster R#6 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#6 S holds
b1 is Correct by Lm67;
end;

Lm68:  for S being Language holds R#7 S is Correct
proofend;

registration
let S be Language;
cluster R#7 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#7 S holds
b1 is Correct by Lm68;
end;

Lm69:  for S being Language holds R#8 S is Correct
proofend;

registration
let S be Language;
cluster R#8 S ->  Correct for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#8 S holds
b1 is Correct by Lm69;
end;

theorem Th16: :: FOMODEL4:16
for S being Language
for D being RuleSet of S st ( for R being Rule of S st R in D holds
R is Correct ) holds
D is Correct
proofend;

registration
let S be Language;
let R be Correct Rule of S;
cluster{R} ->  Correct for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = {R} holds
b1 is Correct
proofend;
end;

registration
let S be Language;
clusterS -rules  ->  Correct for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = S -rules holds
b1 is Correct
proofend;
end;

registration
let S be Language;
cluster R#9 S ->  isotone for Rule of S;
coherence
 for b1 being Rule of S st b1 = R#9 S holds
b1 is isotone
proofend;
end;

registration
let S be Language;
let H be S -premises-like set ;
let phi be wff string of S;
cluster[H,phi] null 1 -> 1,{[H,(xnot (xnot phi))]},{(R#9 S)} -derivable for set ;
coherence
 for b1 being set st b1 = [H,phi] null 1 holds
b1 is 1,{[H,(xnot (xnot phi))]},{(R#9 S)} -derivable
proofend;
end;

registration
let X be set ;
let S be Language;
cluster non empty Relation-like NAT -defined AtomicFormulaSymbolsOf S -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() 0wff 0 -wff wff X -implied for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 ex b1 being 0 -wff string of S st b1 is X -implied
proofend;
end;

registration
let X be set ;
let S be Language;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff X -implied for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 ex b1 being wff string of S st b1 is X -implied
proofend;
end;

registration
let S be Language;
let X be set ;
let phi be wff X -implied string of S;
cluster xnot (xnot phi) ->  wff X -implied for wff string of S;
coherence
 for b1 being wff string of S st b1 = xnot (xnot phi) holds
b1 is X -implied
proofend;
end;

definition
let X be set ;
let S be Language;
let phi be wff string of S;
attrphi is X -provable  means :Def70: :: FOMODEL4:def 70
phi is X,{(R#9 S)} \/ (S -rules) -provable ;
end;

:: deftheorem Def70 defines -provable FOMODEL4:def_70_:_
 for X being set
for S being Language
for phi being wff string of S holds
( phi is X -provable iff phi is X,{(R#9 S)} \/ (S -rules) -provable );

begin

::# constructions for countable languages
::# witness adjoining
definition
let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
set SS = AllSymbolsOf S;
set EF = ExFormulasOf S;
set FF = AllFormulasOf S;
set Y = X \/ (AllFormulasOf S);
set DD = bool (X \/ (AllFormulasOf S));
func(D,num) AddWitnessesTo X ->  Function of NAT,(bool (X \/ (AllFormulasOf S))) means :Def71: :: FOMODEL4:def 71
( it . 0 = X &amp; ( for mm being Element of NAT holds it . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (it . mm) ) );
existence
 ex b1 being Function of NAT,(bool (X \/ (AllFormulasOf S))) st
( b1 . 0 = X &amp; ( for mm being Element of NAT holds b1 . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b1 . mm) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(bool (X \/ (AllFormulasOf S))) st b1 . 0 = X &amp; ( for mm being Element of NAT holds b1 . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b1 . mm) ) &amp; b2 . 0 = X &amp; ( for mm being Element of NAT holds b2 . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b2 . mm) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def71 defines AddWitnessesTo FOMODEL4:def_71_:_
 for X being functional set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(ExFormulasOf S)
for b5 being Function of NAT,(bool (X \/ (AllFormulasOf S))) holds
( b5 = (D,num) AddWitnessesTo X iff ( b5 . 0 = X &amp; ( for mm being Element of NAT holds b5 . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b5 . mm) ) ) );

notation
let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
synonym (D,num) addw X for (D,num) AddWitnessesTo X;
end;

Lm70:  for X being set
for S being Language
for phi being wff string of S
for l1, l2 being literal Element of S
for D being RuleSet of S st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; R#2 S in D &amp; R#5 S in D &amp; X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent &amp; l2 is X \/ {phi} -absent holds
X \/ {(<*l1*> ^ phi)} is D -inconsistent
proofend;

theorem Th17: :: FOMODEL4:17
for k, m being Nat
for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; R#2 S in D &amp; R#5 S in D &amp; (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite &amp; X is D -consistent holds
( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) &amp; (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite &amp; ((D,num) addw X) . m is D -consistent )
proofend;

definition
let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
funcX WithWitnessesFrom (D,num) ->  Subset of (X \/ (AllFormulasOf S)) equals :: FOMODEL4:def 72
 union (rng ((D,num) AddWitnessesTo X));
coherence
 union (rng ((D,num) AddWitnessesTo X)) is Subset of (X \/ (AllFormulasOf S))
proofend;
end;

:: deftheorem  defines WithWitnessesFrom FOMODEL4:def_72_:_
 for X being functional set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(ExFormulasOf S) holds X WithWitnessesFrom (D,num) = union (rng ((D,num) AddWitnessesTo X));

notation
let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
synonym X addw (D,num) for X WithWitnessesFrom (D,num);
end;

Lm71:  for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone &amp; R#1 S in D &amp; R#2 S in D &amp; R#5 S in D &amp; R#8 S in D &amp; (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite &amp; X is D -consistent holds
X addw (D,num) is D -consistent
proofend;

registration
let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
clusterX \ (X addw (D,num)) ->  empty for set ;
coherence
 for b1 being set st b1 = X \ (X addw (D,num)) holds
b1 is empty
proofend;
end;

theorem Th18: :: FOMODEL4:18
for Z being set
for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; R#2 S in D &amp; R#5 S in D &amp; (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite &amp; X addw (D,num) c= Z &amp; Z is D -consistent &amp; rng num = ExFormulasOf S holds
Z is S -witnessed
proofend;

begin

::# constructions for countable languages
::# Consistently maximizing a set of formulas of a countable language
definition
let X be set ;
let S be Language;
let D be RuleSet of S;
let phi be Element of AllFormulasOf S;
func(D,phi) AddFormulaTo X ->  set  equals :Def73: :: FOMODEL4:def 73
X \/ {phi} if  not xnot phi is X,D -provable
otherwise X \/ {(xnot phi)};
consistency
 for b1 being set holds verum ;
coherence
 ( ( not xnot phi is X,D -provable implies X \/ {phi} is set ) &amp; ( xnot phi is X,D -provable implies X \/ {(xnot phi)} is set ) ) ;
end;

:: deftheorem Def73 defines AddFormulaTo FOMODEL4:def_73_:_
 for X being set
for S being Language
for D being RuleSet of S
for phi being Element of AllFormulasOf S holds
( ( not xnot phi is X,D -provable implies (D,phi) AddFormulaTo X = X \/ {phi} ) &amp; ( xnot phi is X,D -provable implies (D,phi) AddFormulaTo X = X \/ {(xnot phi)} ) );

definition
let X be set ;
let S be Language;
let D be RuleSet of S;
let phi be Element of AllFormulasOf S;
:: original:AddFormulaTo
redefine func(D,phi) AddFormulaTo X ->  Subset of (X \/ (AllFormulasOf S));
coherence
 (D,phi) AddFormulaTo X is Subset of (X \/ (AllFormulasOf S))
proofend;
end;

registration
let X be set ;
let S be Language;
let D be RuleSet of S;
let phi be Element of AllFormulasOf S;
clusterX \ ((D,phi) AddFormulaTo X) ->  empty ;
coherence
 X \ ((D,phi) AddFormulaTo X) is empty
proofend;
end;

definition
let X be set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(AllFormulasOf S);
set SS = AllSymbolsOf S;
set FF = AllFormulasOf S;
set Y = X \/ (AllFormulasOf S);
set DD = bool (X \/ (AllFormulasOf S));
func(D,num) AddFormulasTo X ->  Function of NAT,(bool (X \/ (AllFormulasOf S))) means :Def74: :: FOMODEL4:def 74
( it . 0 = X &amp; ( for m being Nat holds it . (m + 1) = (D,(num . m)) AddFormulaTo (it . m) ) );
existence
 ex b1 being Function of NAT,(bool (X \/ (AllFormulasOf S))) st
( b1 . 0 = X &amp; ( for m being Nat holds b1 . (m + 1) = (D,(num . m)) AddFormulaTo (b1 . m) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(bool (X \/ (AllFormulasOf S))) st b1 . 0 = X &amp; ( for m being Nat holds b1 . (m + 1) = (D,(num . m)) AddFormulaTo (b1 . m) ) &amp; b2 . 0 = X &amp; ( for m being Nat holds b2 . (m + 1) = (D,(num . m)) AddFormulaTo (b2 . m) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def74 defines AddFormulasTo FOMODEL4:def_74_:_
 for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S)
for b5 being Function of NAT,(bool (X \/ (AllFormulasOf S))) holds
( b5 = (D,num) AddFormulasTo X iff ( b5 . 0 = X &amp; ( for m being Nat holds b5 . (m + 1) = (D,(num . m)) AddFormulaTo (b5 . m) ) ) );

Lm72:  for k, m being Nat
for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; X is D -consistent holds
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) &amp; ((D,num) AddFormulasTo X) . m is D -consistent )
proofend;

definition
let X be set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(AllFormulasOf S);
func(D,num) CompletionOf X ->  Subset of (X \/ (AllFormulasOf S)) equals :: FOMODEL4:def 75
 union (rng ((D,num) AddFormulasTo X));
coherence
 union (rng ((D,num) AddFormulasTo X)) is Subset of (X \/ (AllFormulasOf S))
proofend;
end;

:: deftheorem  defines CompletionOf FOMODEL4:def_75_:_
 for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) holds (D,num) CompletionOf X = union (rng ((D,num) AddFormulasTo X));

registration
let X be set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(AllFormulasOf S);
clusterX \ ((D,num) CompletionOf X) ->  empty for set ;
coherence
 for b1 being set st b1 = X \ ((D,num) CompletionOf X) holds
b1 is empty
proofend;
end;

Lm73:  for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering
proofend;

Lm74:  for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone &amp; R#1 S in D &amp; R#8 S in D &amp; X is D -consistent holds
(D,num) CompletionOf X is D -consistent
proofend;

theorem :: FOMODEL4:19
for y, X being set
for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . X iff ( y in S -sequents &amp; [X,y] in R ) ) by Lm29;

Lm75:  for S being Language
for D2 being 2 -ranked RuleSet of S
for X being functional set st AllFormulasOf S is countable &amp; (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite &amp; X is D2 -consistent &amp; D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
proofend;

Lm76:  for S being Language
for D2 being 2 -ranked RuleSet of S
for X being functional set st X is finite &amp; AllFormulasOf S is countable &amp; X is D2 -consistent &amp; D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied
proofend;

Lm77:  for U being non empty set
for X being set
for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st S2 is S1 -extending &amp; X c= AllFormulasOf S1 &amp; I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
( X is I1 -satisfied iff X is I2 -satisfied )
proofend;

registration
let S be Language;
let r1, r2 be isotone Rule of S;
cluster{r1,r2} ->  isotone for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = {r1,r2} holds
b1 is isotone
proofend;
end;

registration
let S be Language;
let r1, r2, r3, r4 be isotone Rule of S;
clusterK336(r1,r2,r3,r4) ->  isotone for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = {r1,r2,r3,r4} holds
b1 is isotone
proofend;
end;

registration
let S be Language;
clusterS -rules  ->  isotone for RuleSet of S;
coherence
 for b1 being RuleSet of S st b1 = S -rules holds
b1 is isotone
proofend;
end;

registration
let S be Language;
cluster functional isotone Correct for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being isotone RuleSet of S st b1 is Correct
proofend;
end;

registration
let S be Language;
cluster functional isotone 2 -ranked Correct for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
 ex b1 being isotone Correct RuleSet of S st b1 is 2 -ranked
proofend;
end;

registration
let S be countable Language;
cluster AllFormulasOf S ->  countable ;
coherence
 AllFormulasOf S is countable ;
end;

theorem Th20: :: FOMODEL4:20
for Z being set
for S being countable Language
for D being RuleSet of S st D is 2 -ranked &amp; D is isotone &amp; D is Correct &amp; Z is D -consistent &amp; Z c= AllFormulasOf S holds
ex U being non empty set ex I being Element of U -InterpretersOf S st Z is I -satisfied
proofend;

Lm78:  for Z being set
for S being countable Language
for phi being wff string of S st Z c= AllFormulasOf S &amp; xnot phi is Z -implied holds
xnot phi is Z,S -rules -provable
proofend;

theorem :: FOMODEL4:21
for X being set
for C being countable Language
for phi being wff string of C st X c= AllFormulasOf C &amp; phi is X -implied holds
phi is X -provable
proofend;