:: First order languages: syntax, part two; semantics.
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

definition
let S be Language;
:: original:TheNorSymbOf
redefine func TheNorSymbOf S ->  Element of S;
coherence
 TheNorSymbOf S is Element of S ;
end;

definition
let U be non empty set ;
funcU -deltaInterpreter  ->  Function of (2 -tuples_on U),BOOLEAN equals :: FOMODEL2:def 1
 chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U));
coherence
 chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U)) is Function of (2 -tuples_on U),BOOLEAN ;
end;

:: deftheorem  defines -deltaInterpreter FOMODEL2:def_1_:_
 for U being non empty set holds U -deltaInterpreter = chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U));

definition
let X be set ;
:: original:id
redefine func id X ->  Equivalence_Relation of X;
coherence
 id X is Equivalence_Relation of X by EQREL_1:3;
end;

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
mode Interpreter of s,U ->  set  means :Def2: :: FOMODEL2:def 2
it is Function of ((abs (ar s)) -tuples_on U),BOOLEAN if s is relational
otherwise it is Function of ((abs (ar s)) -tuples_on U),U;
existence
 ( ( s is relational implies ex b1 being set st b1 is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) & ( not s is relational implies ex b1 being set st b1 is Function of ((abs (ar s)) -tuples_on U),U ) )
proofend;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def2 defines Interpreter FOMODEL2:def_2_:_
 for S being Language
for U being non empty set
for s being ofAtomicFormula Element of S
for b4 being set holds
( ( s is relational implies ( b4 is Interpreter of s,U iff b4 is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) ) & ( not s is relational implies ( b4 is Interpreter of s,U iff b4 is Function of ((abs (ar s)) -tuples_on U),U ) ) );

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
:: original:Interpreter
redefine mode Interpreter of s,U ->  Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN);
coherence
 for b1 being Interpreter of s,U holds b1 is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN)
proofend;
end;

registration
let S be Language;
let U be non empty set ;
let s be termal Element of S;
cluster  -> U -valued for Interpreter of s,U;
coherence
 for b1 being Interpreter of s,U holds b1 is U -valued by Def2;
end;

registration
let S be Language;
cluster literal  ->  own for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is literal holds
b1 is own ;
end;

::###############################################################
::###############################################################
::###############################################################
::# Interpreter of a Language.
definition
let S be Language;
let U be non empty set ;
mode Interpreter of S,U ->  Function means :Def3: :: FOMODEL2:def 3
 for s being own Element of S holds it . s is Interpreter of s,U;
existence
 ex b1 being Function st
for s being own Element of S holds b1 . s is Interpreter of s,U
proofend;
end;

:: deftheorem Def3 defines Interpreter FOMODEL2:def_3_:_
 for S being Language
for U being non empty set
for b3 being Function holds
( b3 is Interpreter of S,U iff for s being own Element of S holds b3 . s is Interpreter of s,U );

definition
let S be Language;
let U be non empty set ;
let f be Function;
attrf is S,U -interpreter-like  means :Def4: :: FOMODEL2:def 4
( f is Interpreter of S,U & f is Function-yielding );
end;

:: deftheorem Def4 defines -interpreter-like FOMODEL2:def_4_:_
 for S being Language
for U being non empty set
for f being Function holds
( f is S,U -interpreter-like iff ( f is Interpreter of S,U & f is Function-yielding ) );

registration
let S be Language;
let U be non empty set ;
cluster Relation-like Function-like S,U -interpreter-like  ->  Function-yielding for set ;
coherence
 for b1 being Function st b1 is S,U -interpreter-like holds
b1 is Function-yielding by Def4;
end;

registration
let S be Language;
let U be non empty set ;
let s be own Element of S;
cluster  ->  non empty for Interpreter of s,U;
coherence
 for b1 being Interpreter of s,U holds not b1 is empty ;
end;

Lm1:  for S being Language
for U being non empty set
for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f
proofend;

Lm2:  for S being Language
for U being non empty set
for f being Function st f is S,U -interpreter-like holds
OwnSymbolsOf S c= dom f
proofend;

registration
let S be Language;
let U be non empty set ;
cluster Relation-like Function-like S,U -interpreter-like for set ;
existence
 ex b1 being Function st b1 is S,U -interpreter-like
proofend;
end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let s be own Element of S;
:: original:.
redefine funcI . s ->  Interpreter of s,U;
coherence
 I . s is Interpreter of s,U
proofend;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let x be own Element of S;
let f be Interpreter of x,U;
clusterI +* (x .--> f) -> S,U -interpreter-like ;
coherence
 I +* (x .--> f) is S,U -interpreter-like
proofend;
end;

definition
let f be Function;
let x, y be set ;
func(x,y) ReassignIn f ->  Function equals :: FOMODEL2:def 5
f +* (x .--> ({} .--> y));
coherence
 f +* (x .--> ({} .--> y)) is Function ;
end;

:: deftheorem  defines ReassignIn FOMODEL2:def_5_:_
 for f being Function
for x, y being set holds (x,y) ReassignIn f = f +* (x .--> ({} .--> y));

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let x be literal Element of S;
let u be Element of U;
cluster(x,u) ReassignIn I -> S,U -interpreter-like ;
coherence
 (x,u) ReassignIn I is S,U -interpreter-like
proofend;
end;

::###############################################################
::###############################################################
::###############################################################
registration
let S be Language;
cluster AllSymbolsOf S ->  non empty ;
coherence
 not AllSymbolsOf S is empty ;
end;

registration
let Y be set ;
let X, Z be non empty set ;
cluster Function-like quasi_total  ->  Function-yielding for Element of bool [:X,(Funcs (Y,Z)):];
coherence
 for b1 being Function of X,(Funcs (Y,Z)) holds b1 is Function-yielding ;
end;

registration
let X, Y, Z be non empty set ;
cluster non empty Relation-like X -defined Funcs (Y,Z) -valued Function-like total quasi_total Function-yielding V164() for Element of bool [:X,(Funcs (Y,Z)):];
existence
 ex b1 being Function of X,(Funcs (Y,Z)) st b1 is Function-yielding
proofend;
end;

definition
let f be Function-yielding Function;
let g be Function;
func^^^g,f__ ->  Function means :Def6: :: FOMODEL2:def 6
( dom it = dom f & ( for x being set st x in dom f holds
it . x = g * (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = g * (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = g * (f . x) ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = g * (f . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines ^^^ FOMODEL2:def_6_:_
 for f being Function-yielding Function
for g, b3 being Function holds
( b3 = ^^^g,f__ iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = g * (f . x) ) ) );

registration
let f be empty Function;
let g be Function;
cluster^^^g,f__ ->  empty ;
coherence
 ^^^g,f__ is empty
proofend;
end;

definition
let f be Function-yielding Function;
let g be Function;
func^^^f,g__ ->  Function means :Def7: :: FOMODEL2:def 7
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) . (g . x) ) );
existence
 ex b1 being Function st
( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = (f . x) . (g . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = (f . x) . (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds
b2 . x = (f . x) . (g . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines ^^^ FOMODEL2:def_7_:_
 for f being Function-yielding Function
for g, b3 being Function holds
( b3 = ^^^f,g__ iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in dom b3 holds
b3 . x = (f . x) . (g . x) ) ) );

registration
let f be Function-yielding Function;
let g be empty Function;
cluster^^^f,g__ ->  empty ;
coherence
 ^^^f,g__ is empty
proofend;
end;

registration
let X be FinSequence-membered set ;
cluster Relation-like X -valued Function-like  ->  Function-yielding for set ;
coherence
 for b1 being Function st b1 is X -valued holds
b1 is Function-yielding ;
end;

registration
let E, D be non empty set ;
let p be D -valued FinSequence;
let h be Function of D,E;
clusterh (*) p ->  len p -element for FinSequence;
coherence
 for b1 being FinSequence st b1 = h * p holds
b1 is len p -element
proofend;
end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let p be X -valued FinSequence;
clusterf (*) p ->  FinSequence-like ;
coherence
 f * p is FinSequence-like ;
end;

registration
let E, D be non empty set ;
let n be Nat;
let p be D -valued n -element FinSequence;
let h be Function of D,E;
clusterh (*) p -> n -element for FinSequence of E;
coherence
 for b1 being FinSequence of E st b1 = h * p holds
b1 is n -element ;
end;

Lm3:  for U being non empty set
for S being Language
for I being b2,b1 -interpreter-like Function
for t being termal string of S holds (abs (ar t)) -tuples_on U = dom (I . ((S -firstChar) . t))
by FUNCT_2:def_1;

theorem :: FOMODEL2:1
for S being Language
for t0 being 0 -termal string of S holds t0 = <*((S -firstChar) . t0)*>
proofend;

Lm4:  for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for xx being Function of (AllTermsOf S),U holds
( ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U) &amp; AllTermsOf S c= dom (I * (S -firstChar)) )
proofend;

definition
let S be Language;
let U be non empty set ;
let u be Element of U;
let I be S,U -interpreter-like Function;
func(I,u) -TermEval  ->  Function of NAT,(Funcs ((AllTermsOf S),U)) means :Def8: :: FOMODEL2:def 8
( it . 0 = (AllTermsOf S) --> u &amp; ( for mm being Element of NAT holds it . (mm + 1) = ^^^(I * (S -firstChar)),^^^(it . mm),(S -subTerms)____ ) );
existence
 ex b1 being Function of NAT,(Funcs ((AllTermsOf S),U)) st
( b1 . 0 = (AllTermsOf S) --> u &amp; ( for mm being Element of NAT holds b1 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b1 . mm),(S -subTerms)____ ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(Funcs ((AllTermsOf S),U)) st b1 . 0 = (AllTermsOf S) --> u &amp; ( for mm being Element of NAT holds b1 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b1 . mm),(S -subTerms)____ ) &amp; b2 . 0 = (AllTermsOf S) --> u &amp; ( for mm being Element of NAT holds b2 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b2 . mm),(S -subTerms)____ ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines -TermEval FOMODEL2:def_8_:_
 for S being Language
for U being non empty set
for u being Element of U
for I being b1,b2 -interpreter-like Function
for b5 being Function of NAT,(Funcs ((AllTermsOf S),U)) holds
( b5 = (I,u) -TermEval iff ( b5 . 0 = (AllTermsOf S) --> u &amp; ( for mm being Element of NAT holds b5 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b5 . mm),(S -subTerms)____ ) ) );

Lm5:  for S being Language
for U being non empty set
for u being Element of U
for I being b1,b2 -interpreter-like Function
for t being termal string of S
for mm being Element of NAT holds
( (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) &amp; ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )
proofend;

Lm6:  for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for u1, u2 being Element of U
for m being Nat
for t being b6 -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t
proofend;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let t be Element of AllTermsOf S;
funcI -TermEval t ->  Element of U means :Def9: :: FOMODEL2:def 9
 for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
it = (((I,u1) -TermEval) . (mm + 1)) . t;
existence
 ex b1 being Element of U st
for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b1 = (((I,u1) -TermEval) . (mm + 1)) . t
proofend;
uniqueness
 for b1, b2 being Element of U st ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b1 = (((I,u1) -TermEval) . (mm + 1)) . t ) &amp; ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b2 = (((I,u1) -TermEval) . (mm + 1)) . t ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines -TermEval FOMODEL2:def_9_:_
 for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for t being Element of AllTermsOf S
for b5 being Element of U holds
( b5 = I -TermEval t iff for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b5 = (((I,u1) -TermEval) . (mm + 1)) . t );

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
funcI -TermEval  ->  Function of (AllTermsOf S),U means :Def10: :: FOMODEL2:def 10
 for t being Element of AllTermsOf S holds it . t = I -TermEval t;
existence
 ex b1 being Function of (AllTermsOf S),U st
for t being Element of AllTermsOf S holds b1 . t = I -TermEval t
proofend;
uniqueness
 for b1, b2 being Function of (AllTermsOf S),U st ( for t being Element of AllTermsOf S holds b1 . t = I -TermEval t ) &amp; ( for t being Element of AllTermsOf S holds b2 . t = I -TermEval t ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines -TermEval FOMODEL2:def_10_:_
 for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for b4 being Function of (AllTermsOf S),U holds
( b4 = I -TermEval iff for t being Element of AllTermsOf S holds b4 . t = I -TermEval t );

::############### Semantics of 0wff formulas (propositions) ############
::#########################################################################
definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
funcI ===  ->  Function equals :: FOMODEL2:def 11
I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter));
coherence
 I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter)) is Function ;
end;

:: deftheorem  defines === FOMODEL2:def_11_:_
 for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function holds I === = I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter));

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let x be set ;
attrx is I -extension  means :Def12: :: FOMODEL2:def 12
x = I === ;
end;

:: deftheorem Def12 defines -extension FOMODEL2:def_12_:_
 for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for x being set holds
( x is I -extension iff x = I === );

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
clusterI ===  -> I -extension for Function;
coherence
 for b1 being Function st b1 = I === holds
b1 is I -extension by Def12;
clusterI -extension  ->  Function-like for set ;
coherence
 for b1 being set st b1 is I -extension holds
b1 is Function-like
proofend;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster Relation-like Function-like I -extension for set ;
existence
 ex b1 being Function st b1 is I -extension
proofend;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
clusterI ===  -> S,U -interpreter-like ;
coherence
 I === is S,U -interpreter-like
proofend;
end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let f be I -extension Function;
let s be ofAtomicFormula Element of S;
:: original:.
redefine funcf . s ->  Interpreter of s,U;
coherence
 f . s is Interpreter of s,U
proofend;
end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let phi be 0wff string of S;
funcI -AtomicEval phi ->  set  equals :: FOMODEL2:def 13
((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi));
coherence
 ((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) is set ;
end;

:: deftheorem  defines -AtomicEval FOMODEL2:def_13_:_
 for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for phi being 0wff string of S holds I -AtomicEval phi = ((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi));

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let phi be 0wff string of S;
:: original:-AtomicEval
redefine funcI -AtomicEval phi ->  Element of BOOLEAN ;
coherence
 I -AtomicEval phi is Element of BOOLEAN
proofend;
end;

::###### Semantics of formulas (evaluation of any wff string) ##########
::######################################################################
registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
clusterI | (OwnSymbolsOf S) ->  PFuncs ((U *),(U \/ BOOLEAN)) -valued for Function;
coherence
 for b1 being Function st b1 = I | (OwnSymbolsOf S) holds
b1 is PFuncs ((U *),(U \/ BOOLEAN)) -valued
proofend;
clusterI | (OwnSymbolsOf S) -> S,U -interpreter-like for Function;
coherence
 for b1 being Function st b1 = I | (OwnSymbolsOf S) holds
b1 is S,U -interpreter-like
proofend;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
clusterI | (OwnSymbolsOf S) ->  OwnSymbolsOf S -defined total for OwnSymbolsOf S -defined Relation;
coherence
 for b1 being OwnSymbolsOf S -defined Relation st b1 = I | (OwnSymbolsOf S) holds
b1 is total
proofend;
end;

definition
let S be Language;
let U be non empty set ;
funcU -InterpretersOf S ->  set  equals :: FOMODEL2:def 14
 {  f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like  }  ;
coherence
  {  f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like  }  is set ;
end;

:: deftheorem  defines -InterpretersOf FOMODEL2:def_14_:_
 for S being Language
for U being non empty set holds U -InterpretersOf S =  {  f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like  }  ;

definition
let S be Language;
let U be non empty set ;
:: original:-InterpretersOf
redefine funcU -InterpretersOf S ->  Subset of (Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))));
coherence
 U -InterpretersOf S is Subset of (Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))))
proofend;
end;

registration
let S be Language;
let U be non empty set ;
clusterU -InterpretersOf S ->  non empty ;
coherence
 not U -InterpretersOf S is empty
proofend;
end;

registration
let S be Language;
let U be non empty set ;
cluster  -> S,U -interpreter-like for Element of U -InterpretersOf S;
coherence
 for b1 being Element of U -InterpretersOf S holds b1 is S,U -interpreter-like
proofend;
end;

definition
let S be Language;
let U be non empty set ;
funcS -TruthEval U ->  Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN means :Def15: :: FOMODEL2:def 15
 for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds it . (I,phi) = I -AtomicEval phi;
existence
 ex b1 being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN st
for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b1 . (I,phi) = I -AtomicEval phi
proofend;
uniqueness
 for b1, b2 being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN st ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b1 . (I,phi) = I -AtomicEval phi ) &amp; ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b2 . (I,phi) = I -AtomicEval phi ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines -TruthEval FOMODEL2:def_15_:_
 for S being Language
for U being non empty set
for b3 being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN holds
( b3 = S -TruthEval U iff for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b3 . (I,phi) = I -AtomicEval phi );

definition
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let f be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN;
let phi be Element of ((AllSymbolsOf S) *) \ {{}};
funcf -ExFunctor (I,phi) ->  Element of BOOLEAN  equals :Def16: :: FOMODEL2:def 16
 TRUE  if  ex u being Element of U ex v being literal Element of S st
( phi . 1 = v &amp; f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE )
otherwise  FALSE ;
coherence
 ( ( ex u being Element of U ex v being literal Element of S st
( phi . 1 = v &amp; f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) implies TRUE is Element of BOOLEAN ) &amp; ( ( for u being Element of U
for v being literal Element of S holds
( not phi . 1 = v or not f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) ) implies FALSE is Element of BOOLEAN ) ) ;
consistency
 for b1 being Element of BOOLEAN holds verum ;
end;

:: deftheorem Def16 defines -ExFunctor FOMODEL2:def_16_:_
 for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN
for phi being Element of ((AllSymbolsOf S) *) \ {{}} holds
( ( ex u being Element of U ex v being literal Element of S st
( phi . 1 = v &amp; f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) implies f -ExFunctor (I,phi) = TRUE ) &amp; ( ( for u being Element of U
for v being literal Element of S holds
( not phi . 1 = v or not f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) ) implies f -ExFunctor (I,phi) = FALSE ) );

definition
let S be Language;
let U be non empty set ;
let g be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN);
func ExIterator g ->  PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN means :Def17: :: FOMODEL2:def 17
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom it iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g &amp; y = <*v*> ^ w ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom it holds
it . (x,y) = g -ExFunctor (x,y) ) );
existence
 ex b1 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g &amp; y = <*v*> ^ w ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -ExFunctor (x,y) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g &amp; y = <*v*> ^ w ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -ExFunctor (x,y) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b2 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g &amp; y = <*v*> ^ w ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b2 holds
b2 . (x,y) = g -ExFunctor (x,y) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines ExIterator FOMODEL2:def_17_:_
 for S being Language
for U being non empty set
for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)
for b4 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b4 = ExIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b4 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g &amp; y = <*v*> ^ w ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b4 holds
b4 . (x,y) = g -ExFunctor (x,y) ) ) );

definition
let S be Language;
let U be non empty set ;
let f be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN;
let I be Element of U -InterpretersOf S;
let phi be Element of ((AllSymbolsOf S) *) \ {{}};
funcf -NorFunctor (I,phi) ->  Element of BOOLEAN  equals :Def18: :: FOMODEL2:def 18
 TRUE  if  ex w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( [I,w1] in dom f &amp; f . (I,w1) = FALSE &amp; f . (I,w2) = FALSE &amp; phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 )
otherwise  FALSE ;
coherence
 ( ( ex w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( [I,w1] in dom f &amp; f . (I,w1) = FALSE &amp; f . (I,w2) = FALSE &amp; phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) implies TRUE is Element of BOOLEAN ) &amp; ( ( for w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) ) implies FALSE is Element of BOOLEAN ) ) ;
consistency
 for b1 being Element of BOOLEAN holds verum ;
end;

:: deftheorem Def18 defines -NorFunctor FOMODEL2:def_18_:_
 for S being Language
for U being non empty set
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN
for I being Element of U -InterpretersOf S
for phi being Element of ((AllSymbolsOf S) *) \ {{}} holds
( ( ex w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( [I,w1] in dom f &amp; f . (I,w1) = FALSE &amp; f . (I,w2) = FALSE &amp; phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) implies f -NorFunctor (I,phi) = TRUE ) &amp; ( ( for w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) ) implies f -NorFunctor (I,phi) = FALSE ) );

::# The inelegant specification [I,w1] in dom f above is needed because
::# of a general problem with the . functor Despite the ideal policy of
::# separating the definition of well-formedness and truth value respectively
::# in NorIterator and -NorFunctor, one is obliged to repeat the specification
::# because the . functor adopts {} as return value for indefinite arguments
::# (see FUNCT_1:def 4) Sadly, {} is also the set conventionally chosen to
::# represent FALSE (and many other things), so we cannot resolve ambiguity
::# between a meaningless argument and a false argument, and are forced to
::# add the statement about the argument effectively belonging to the domain.
::# An alternative could have been to recode truth values in e.g. 1=true,
::# 2=false, but that could have been too much of a breakthrough. Thus in
::# general, when one has to choose an arbitrary convention to represent
::# things, I feel it would be better to avoid functions with 0={} in their
::# ranges; sadly this does not happen in many cases (see eg the chi functor),
::# probably because of the load of intuitive, symbolic, representative
::# imagery that 0 and emptiness symbols convey.
definition
let S be Language;
let U be non empty set ;
let g be Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN);
func NorIterator g ->  PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN means :Def19: :: FOMODEL2:def 19
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom it iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; [x,phi1] in dom g &amp; [x,phi2] in dom g ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom it holds
it . (x,y) = g -NorFunctor (x,y) ) );
existence
 ex b1 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; [x,phi1] in dom g &amp; [x,phi2] in dom g ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -NorFunctor (x,y) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; [x,phi1] in dom g &amp; [x,phi2] in dom g ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -NorFunctor (x,y) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b2 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; [x,phi1] in dom g &amp; [x,phi2] in dom g ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b2 holds
b2 . (x,y) = g -NorFunctor (x,y) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines NorIterator FOMODEL2:def_19_:_
 for S being Language
for U being non empty set
for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)
for b4 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b4 = NorIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b4 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 &amp; [x,phi1] in dom g &amp; [x,phi2] in dom g ) ) ) &amp; ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b4 holds
b4 . (x,y) = g -NorFunctor (x,y) ) ) );

definition
let S be Language;
let U be non empty set ;
func(S,U) -TruthEval  ->  Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) means :Def20: :: FOMODEL2:def 20
( it . 0 = S -TruthEval U &amp; ( for mm being Element of NAT holds it . (mm + 1) = ((ExIterator (it . mm)) +* (NorIterator (it . mm))) +* (it . mm) ) );
existence
 ex b1 being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st
( b1 . 0 = S -TruthEval U &amp; ( for mm being Element of NAT holds b1 . (mm + 1) = ((ExIterator (b1 . mm)) +* (NorIterator (b1 . mm))) +* (b1 . mm) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st b1 . 0 = S -TruthEval U &amp; ( for mm being Element of NAT holds b1 . (mm + 1) = ((ExIterator (b1 . mm)) +* (NorIterator (b1 . mm))) +* (b1 . mm) ) &amp; b2 . 0 = S -TruthEval U &amp; ( for mm being Element of NAT holds b2 . (mm + 1) = ((ExIterator (b2 . mm)) +* (NorIterator (b2 . mm))) +* (b2 . mm) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines -TruthEval FOMODEL2:def_20_:_
 for S being Language
for U being non empty set
for b3 being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) holds
( b3 = (S,U) -TruthEval iff ( b3 . 0 = S -TruthEval U &amp; ( for mm being Element of NAT holds b3 . (mm + 1) = ((ExIterator (b3 . mm)) +* (NorIterator (b3 . mm))) +* (b3 . mm) ) ) );

theorem Th2: :: FOMODEL2:2
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S
proofend;

definition
let S be Language;
let m be Nat;
let U be non empty set ;
func(S,U) -TruthEval m ->  Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) means :Def21: :: FOMODEL2:def 21
 for mm being Element of NAT st m = mm holds
it = ((S,U) -TruthEval) . mm;
existence
 ex b1 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st
for mm being Element of NAT st m = mm holds
b1 = ((S,U) -TruthEval) . mm
proofend;
uniqueness
 for b1, b2 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st ( for mm being Element of NAT st m = mm holds
b1 = ((S,U) -TruthEval) . mm ) &amp; ( for mm being Element of NAT st m = mm holds
b2 = ((S,U) -TruthEval) . mm ) holds
b1 = b2
proofend;
end;

:: deftheorem Def21 defines -TruthEval FOMODEL2:def_21_:_
 for S being Language
for m being Nat
for U being non empty set
for b4 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) holds
( b4 = (S,U) -TruthEval m iff for mm being Element of NAT st m = mm holds
b4 = ((S,U) -TruthEval) . mm );

Lm7:  for m being Nat
for x being set
for S being Language
for U being non empty set
for n being Nat st x in dom ((S,U) -TruthEval m) holds
( x in dom ((S,U) -TruthEval (m + n)) &amp; ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + n)) . x )
proofend;

Lm8:  for x, X, Y, Z being set holds
( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) )
proofend;

Lm9:  for S being Language
for U1, U2 being non empty set
for m being Nat
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval m) holds
[I2,w] in dom ((S,U2) -TruthEval m)
proofend;

Lm10:  for mm being Element of NAT
for S being Language
for U being non empty set holds curry (((S,U) -TruthEval) . mm) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
proofend;

Lm11:  for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
proofend;

definition
let S be Language;
let U be non empty set ;
let m be Nat;
let I be Element of U -InterpretersOf S;
func(I,m) -TruthEval  ->  Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN) equals :: FOMODEL2:def 22
(curry ((S,U) -TruthEval m)) . I;
coherence
 (curry ((S,U) -TruthEval m)) . I is Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)
proofend;
end;

:: deftheorem  defines -TruthEval FOMODEL2:def_22_:_
 for S being Language
for U being non empty set
for m being Nat
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval = (curry ((S,U) -TruthEval m)) . I;

Lm12:  for m, n being Nat
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval c= (I,(m + n)) -TruthEval
proofend;

Lm13:  for m being Nat
for S being Language
for U1, U2 being non empty set
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
proofend;

Lm14:  for mm being Element of NAT
for S being Language
for U1, U2 being non empty set
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,mm) -TruthEval) = dom ((I2,mm) -TruthEval)
proofend;

definition
let S be Language;
let m be Nat;
funcS -formulasOfMaxDepth m ->  Subset of (((AllSymbolsOf S) *) \ {{}}) means :Def23: :: FOMODEL2:def 23
 for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
it = dom ((I,mm) -TruthEval);
existence
 ex b1 being Subset of (((AllSymbolsOf S) *) \ {{}}) st
for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b1 = dom ((I,mm) -TruthEval)
proofend;
uniqueness
 for b1, b2 being Subset of (((AllSymbolsOf S) *) \ {{}}) st ( for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b1 = dom ((I,mm) -TruthEval) ) &amp; ( for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b2 = dom ((I,mm) -TruthEval) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def23 defines -formulasOfMaxDepth FOMODEL2:def_23_:_
 for S being Language
for m being Nat
for b3 being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b3 = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b3 = dom ((I,mm) -TruthEval) );

Lm15:  for m, n being Nat
for S being Language holds S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n)
proofend;

Lm16:  for S being Language holds S -formulasOfMaxDepth 0 = AtomicFormulasOf S
proofend;

definition
let S be Language;
let m be Nat;
let w be string of S;
attrw is m -wff  means :Def24: :: FOMODEL2:def 24
w in S -formulasOfMaxDepth m;
end;

:: deftheorem Def24 defines -wff FOMODEL2:def_24_:_
 for S being Language
for m being Nat
for w being string of S holds
( w is m -wff iff w in S -formulasOfMaxDepth m );

definition
let S be Language;
let w be string of S;
attrw is wff  means :Def25: :: FOMODEL2:def 25
 ex m being Nat st w is m -wff ;
end;

:: deftheorem Def25 defines wff FOMODEL2:def_25_:_
 for S being Language
for w being string of S holds
( w is wff iff ex m being Nat st w is m -wff );

registration
let S be Language;
cluster 0 -wff  ->  0wff for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st b1 is 0 -wff holds
b1 is 0wff
proofend;
cluster 0wff  ->  0 -wff for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st b1 is 0wff holds
b1 is 0 -wff
proofend;
let m be Nat;
clusterm -wff  ->  wff for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st b1 is m -wff holds
b1 is wff by Def25;
let n be Nat;
clusterm + (0 * n) -wff  -> m + n -wff for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st b1 is m + (0 * n) -wff holds
b1 is m + n -wff
proofend;
end;

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

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

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

definition
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let w be wff string of S;
funcI -TruthEval w ->  Element of BOOLEAN  means :Def26: :: FOMODEL2:def 26
 for m being Nat st w is m -wff holds
it = ((I,m) -TruthEval) . w;
existence
 ex b1 being Element of BOOLEAN st
for m being Nat st w is m -wff holds
b1 = ((I,m) -TruthEval) . w
proofend;
uniqueness
 for b1, b2 being Element of BOOLEAN st ( for m being Nat st w is m -wff holds
b1 = ((I,m) -TruthEval) . w ) &amp; ( for m being Nat st w is m -wff holds
b2 = ((I,m) -TruthEval) . w ) holds
b1 = b2
proofend;
end;

:: deftheorem Def26 defines -TruthEval FOMODEL2:def_26_:_
 for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S
for w being wff string of S
for b5 being Element of BOOLEAN holds
( b5 = I -TruthEval w iff for m being Nat st w is m -wff holds
b5 = ((I,m) -TruthEval) . w );

definition
let S be Language;
func AllFormulasOf S ->  set  equals :: FOMODEL2:def 27
 {  w where w is string of S : ex m being Nat st w is m -wff  }  ;
coherence
  {  w where w is string of S : ex m being Nat st w is m -wff  }  is set ;
end;

:: deftheorem  defines AllFormulasOf FOMODEL2:def_27_:_
 for S being Language holds AllFormulasOf S =  {  w where w is string of S : ex m being Nat st w is m -wff  }  ;

registration
let S be Language;
cluster AllFormulasOf S ->  non empty ;
coherence
 not AllFormulasOf S is empty
proofend;
end;

theorem Th3: :: FOMODEL2:3
for m being Nat
for S being Language
for U being non empty set
for u being Element of U
for t being termal string of S
for I being b2,b3 -interpreter-like Function holds
( (((I,u) -TermEval) . (m + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . m) * (SubTerms t)) &amp; ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )
proofend;

theorem :: FOMODEL2:4
for m, n being Nat
for S being Language
for U being non empty set
for u1, u2 being Element of U
for I being b3,b4 -interpreter-like Function
for t being b1 -termal string of S holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t by Lm6;

theorem :: FOMODEL2:5
for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)) by Lm11;

theorem :: FOMODEL2:6
for x, X, Y, Z being set holds
( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) ) by Lm8;

theorem :: FOMODEL2:7
for S being Language holds S -formulasOfMaxDepth 0 = AtomicFormulasOf S by Lm16;

definition
let S be Language;
let m be Nat;
redefine func S -formulasOfMaxDepth m means :Def28: :: FOMODEL2:def 28
 for U being non empty set
for I being Element of U -InterpretersOf S holds it = dom ((I,m) -TruthEval);
compatibility
 for b1 being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b1 = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b1 = dom ((I,m) -TruthEval) )
proofend;
end;

:: deftheorem Def28 defines -formulasOfMaxDepth FOMODEL2:def_28_:_
 for S being Language
for m being Nat
for b3 being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b3 = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b3 = dom ((I,m) -TruthEval) );

Lm17:  for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN))
proofend;

theorem Th8: :: FOMODEL2:8
for m being Nat
for S being Language
for U being non empty set holds
( (S,U) -TruthEval m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) &amp; ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) )
proofend;

definition
let S be Language;
let m be Nat;
funcm -ExFormulasOf S ->  set  equals :: FOMODEL2:def 29
 {  (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum  }  ;
coherence
  {  (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum  }  is set ;
funcm -NorFormulasOf S ->  set  equals :: FOMODEL2:def 30
 {  ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum  }  ;
coherence
  {  ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum  }  is set ;
end;

:: deftheorem  defines -ExFormulasOf FOMODEL2:def_29_:_
 for S being Language
for m being Nat holds m -ExFormulasOf S =  {  (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum  }  ;

:: deftheorem  defines -NorFormulasOf FOMODEL2:def_30_:_
 for S being Language
for m being Nat holds m -NorFormulasOf S =  {  ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum  }  ;

definition
let S be Language;
let w1, w2 be string of S;
:: original:^
redefine funcw1 ^ w2 ->  string of S;
coherence
 w1 ^ w2 is string of S
proofend;
end;

definition
let S be Language;
let s be Element of S;
:: original:<*
redefine func<*s*> ->  string of S;
coherence
 <*s*> is string of S
proofend;
end;

Lm18:  for m being Nat
for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
proofend;

Lm19:  for m being Nat
for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):]
proofend;

theorem Th9: :: FOMODEL2:9
for m being Nat
for S being Language holds S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)
proofend;

theorem Th10: :: FOMODEL2:10
for S being Language holds AtomicFormulasOf S is S -prefix
proofend;

registration
let S be Language;
cluster AtomicFormulasOf S -> S -prefix for set ;
coherence
 for b1 being set st b1 = AtomicFormulasOf S holds
b1 is S -prefix by Th10;
end;

registration
let S be Language;
clusterS -formulasOfMaxDepth 0 -> S -prefix for set ;
coherence
 for b1 being set st b1 = S -formulasOfMaxDepth 0 holds
b1 is S -prefix
proofend;
end;

definition
let S be Language;
let phi be wff string of S;
func Depth phi ->  Nat means :Def31: :: FOMODEL2:def 31
( phi is it -wff &amp; ( for n being Nat st phi is n -wff holds
it <= n ) );
existence
 ex b1 being Nat st
( phi is b1 -wff &amp; ( for n being Nat st phi is n -wff holds
b1 <= n ) )
proofend;
uniqueness
 for b1, b2 being Nat st phi is b1 -wff &amp; ( for n being Nat st phi is n -wff holds
b1 <= n ) &amp; phi is b2 -wff &amp; ( for n being Nat st phi is n -wff holds
b2 <= n ) holds
b1 = b2
proofend;
end;

:: deftheorem Def31 defines Depth FOMODEL2:def_31_:_
 for S being Language
for phi being wff string of S
for b3 being Nat holds
( b3 = Depth phi iff ( phi is b3 -wff &amp; ( for n being Nat st phi is n -wff holds
b3 <= n ) ) );

Lm20:  for m being Nat
for S being Language
for phi being wff string of S st phi in (S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0) holds
ex n being Nat st
( phi is n + 1 -wff &amp; not phi is n -wff &amp; n + 1 <= m )
proofend;

Lm21:  for m being Nat
for S being Language
for w being string of S st w is m + 1 -wff &amp; not w is m -wff &amp; ( for v being literal Element of S
for phi being b1 -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being b1 -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
proofend;

registration
let S be Language;
let m be Nat;
let phi1, phi2 be m -wff string of S;
cluster(<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> m + 1 -wff for string of S;
coherence
 for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is m + 1 -wff
proofend;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster(<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ->  wff for string of S;
coherence
 for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is wff
proofend;
end;

registration
let S be Language;
let m be Nat;
let phi be m -wff string of S;
let v be literal Element of S;
cluster<*v*> ^ phi -> m + 1 -wff for string of S;
coherence
 for b1 being string of S st b1 = <*v*> ^ phi holds
b1 is m + 1 -wff
proofend;
end;

registration
let S be Language;
let l be literal Element of S;
let phi be wff string of S;
cluster<*l*> ^ phi ->  wff for string of S;
coherence
 for b1 being string of S st b1 = <*l*> ^ phi holds
b1 is wff
proofend;
end;

registration
let S be Language;
let w be string of S;
let s be non relational Element of S;
cluster<*s*> ^ w ->  non 0wff for string of S;
coherence
 for b1 being string of S st b1 = <*s*> ^ w holds
not b1 is 0wff
proofend;
end;

registration
let S be Language;
let w1, w2 be string of S;
let s be non relational Element of S;
cluster(<*s*> ^ w1) ^ w2 ->  non 0wff for string of S;
coherence
 for b1 being string of S st b1 = (<*s*> ^ w1) ^ w2 holds
not b1 is 0wff
proofend;
end;

registration
let S be Language;
cluster TheNorSymbOf S ->  non relational for Element of S;
coherence
 for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is relational ;
end;

registration
let S be Language;
let w be string of S;
cluster<*(TheNorSymbOf S)*> ^ w ->  non 0wff for string of S;
coherence
 for b1 being string of S st b1 = <*(TheNorSymbOf S)*> ^ w holds
not b1 is 0wff ;
end;

registration
let S be Language;
let l be literal Element of S;
let w be string of S;
cluster<*l*> ^ w ->  non 0wff for string of S;
coherence
 for b1 being string of S st b1 = <*l*> ^ w holds
not b1 is 0wff ;
end;

definition
let S be Language;
let w be string of S;
attrw is exal  means :Def32: :: FOMODEL2:def 32
(S -firstChar) . w is literal ;
end;

:: deftheorem Def32 defines exal FOMODEL2:def_32_:_
 for S being Language
for w being string of S holds
( w is exal iff (S -firstChar) . w is literal );

registration
let S be Language;
let w be string of S;
let l be literal Element of S;
cluster<*l*> ^ w ->  exal for string of S;
coherence
 for b1 being string of S st b1 = <*l*> ^ w holds
b1 is exal
proofend;
end;

registration
let S be Language;
let m1 be non zero Nat;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V199() m1 -wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 ex b1 being m1 -wff string of S st b1 is exal
proofend;
end;

registration
let S be Language;
cluster exal  ->  non 0wff for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st b1 is exal holds
not b1 is 0wff
proofend;
end;

registration
let S be Language;
let m1 be non zero Nat;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V199() non 0wff m1 -wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 not for b1 being m1 -wff exal string of S holds b1 is 0wff
proofend;
end;

registration
let S be Language;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V199() non 0wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 not for b1 being wff exal string of S holds b1 is 0wff
proofend;
end;

Lm22:  for S being Language
for phi being wff string of S st not phi is 0wff holds
Depth phi <> 0
proofend;

registration
let S be Language;
let phi be non 0wff wff string of S;
cluster Depth phi ->  non zero for Nat;
coherence
 for b1 being Nat st b1 = Depth phi holds
not b1 is empty by Lm22;
end;

Lm23:  for S being Language
for w being string of S st w is wff &amp; not w is 0wff &amp; not w . 1 in LettersOf S holds
w . 1 = TheNorSymbOf S
proofend;

registration
let S be Language;
let w be non 0wff wff string of S;
cluster(S -firstChar) . w ->  non relational for Element of S;
coherence
 for b1 being Element of S st b1 = (S -firstChar) . w holds
not b1 is relational
proofend;
end;

Lm24:  for m being Nat
for S being Language holds S -formulasOfMaxDepth m is S -prefix
proofend;

registration
let S be Language;
let m be Nat;
clusterS -formulasOfMaxDepth m -> S -prefix for set ;
coherence
 for b1 being set st b1 = S -formulasOfMaxDepth m holds
b1 is S -prefix by Lm24;
end;

definition
let S be Language;
:: original:AllFormulasOf
redefine func AllFormulasOf S ->  Subset of (((AllSymbolsOf S) *) \ {{}});
coherence
 AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
proofend;
end;

registration
let S be Language;
cluster  ->  wff for Element of AllFormulasOf S;
coherence
 for b1 being Element of AllFormulasOf S holds b1 is wff
proofend;
end;

Lm25:  for S being Language holds AllFormulasOf S is S -prefix
proofend;

registration
let S be Language;
cluster AllFormulasOf S -> S -prefix for set ;
coherence
 for b1 being set st b1 = AllFormulasOf S holds
b1 is S -prefix by Lm25;
end;

theorem :: FOMODEL2:11
for m being Nat
for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):] by Lm18;

theorem :: FOMODEL2:12
for m being Nat
for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):] by Lm19;

Lm26:  for U being non empty set holds (U -deltaInterpreter) " {1} = (U -concatenation) .: (id (1 -tuples_on U))
proofend;

theorem Th13: :: FOMODEL2:13
for U being non empty set holds (U -deltaInterpreter) " {1} =  {  <*u,u*> where u is Element of U : verum  }
proofend;

definition
let S be Language;
:: original:TheEqSymbOf
redefine func TheEqSymbOf S ->  Element of S;
coherence
 TheEqSymbOf S is Element of S ;
end;

registration
let S be Language;
cluster(ar (TheEqSymbOf S)) + 2 ->  zero for number ;
coherence
 for b1 being number st b1 = (ar (TheEqSymbOf S)) + 2 holds
b1 is empty
proofend;
cluster(abs (ar (TheEqSymbOf S))) - 2 ->  zero for number ;
coherence
 for b1 being number st b1 = (abs (ar (TheEqSymbOf S))) - 2 holds
b1 is empty
proofend;
end;

theorem Th14: :: FOMODEL2:14
for S being Language
for U being non empty set
for phi being 0wff string of S
for I being b1,b2 -interpreter-like Function holds
( ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) &amp; ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ) )
proofend;

theorem :: FOMODEL2:15
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
proofend;

registration
let S be Language;
let m be Nat;
clusterm -ExFormulasOf S ->  non empty for set ;
coherence
 for b1 being set st b1 = m -ExFormulasOf S holds
not b1 is empty
proofend;
end;

registration
let S be Language;
let m be Nat;
clusterm -NorFormulasOf S ->  non empty for set ;
coherence
 for b1 being set st b1 = m -NorFormulasOf S holds
not b1 is empty
proofend;
end;

definition
let S be Language;
let m be Nat;
:: original:-NorFormulasOf
redefine funcm -NorFormulasOf S ->  Subset of (((AllSymbolsOf S) *) \ {{}});
coherence
 m -NorFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
proofend;
end;

registration
let S be Language;
let w be exal string of S;
cluster(S -firstChar) . w ->  literal for Element of S;
coherence
 for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is literal by Def32;
end;

registration
let S be Language;
let m be Nat;
cluster  ->  non exal for Element of m -NorFormulasOf S;
coherence
 for b1 being Element of m -NorFormulasOf S holds not b1 is exal
proofend;
end;

Lm27:  for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 &amp; phi is exal holds
phi in m -ExFormulasOf S
proofend;

Lm28:  for S being Language
for l being literal Element of S
for phi1 being wff string of S holds Depth (<*l*> ^ phi1) > Depth phi1
proofend;

definition
let S be Language;
let m be Nat;
:: original:-ExFormulasOf
redefine funcm -ExFormulasOf S ->  Subset of (((AllSymbolsOf S) *) \ {{}});
coherence
 m -ExFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
proofend;
end;

registration
let S be Language;
let m be Nat;
cluster  ->  exal for Element of m -ExFormulasOf S;
coherence
 for b1 being Element of m -ExFormulasOf S holds b1 is exal
proofend;
end;

Lm29:  for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 &amp; not phi is exal holds
phi in m -NorFormulasOf S
proofend;

registration
let S be Language;
cluster non literal for Element of AllSymbolsOf S;
existence
 not for b1 being Element of S holds b1 is literal
proofend;
end;

registration
let S be Language;
let w be string of S;
let s be non literal Element of S;
cluster<*s*> ^ w ->  non exal for string of S;
coherence
 for b1 being string of S st b1 = <*s*> ^ w holds
not b1 is exal
proofend;
end;

registration
let S be Language;
let w1, w2 be string of S;
let s be non literal Element of S;
cluster(<*s*> ^ w1) ^ w2 ->  non exal for string of S;
coherence
 for b1 being string of S st b1 = (<*s*> ^ w1) ^ w2 holds
not b1 is exal
proofend;
end;

registration
let S be Language;
cluster TheNorSymbOf S ->  non literal for Element of S;
coherence
 for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is literal ;
end;

theorem Th16: :: FOMODEL2:16
for S being Language
for phi being wff string of S holds phi in AllFormulasOf S
proofend;

Lm30:  for S being Language
for phi1, phi2 being wff string of S holds
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 &amp; Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 )
proofend;

Lm31:  for S being Language
for phi1, phi2 being wff string of S holds Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
proofend;

notation
let S be Language;
let m be Nat;
let w be string of S;
antonym m -nonwff w for m -wff ;
end;

registration
let m be Nat;
let S be Language;
cluster non m -wff  -> m -nonwff for Element of ((AllSymbolsOf S) *) \ {{}};
coherence
 for b1 being string of S st not b1 is m -wff holds
b1 is m -nonwff ;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster(<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ->  max ((Depth phi1),(Depth phi2)) -nonwff for string of S;
coherence
 for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
not b1 is max ((Depth phi1),(Depth phi2)) -wff
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
let l be literal Element of S;
cluster<*l*> ^ phi ->  Depth phi -nonwff for string of S;
coherence
 for b1 being string of S st b1 = <*l*> ^ phi holds
not b1 is Depth phi -wff
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
let l be literal Element of S;
cluster<*l*> ^ phi -> 1 + (Depth phi) -wff for string of S;
coherence
 for b1 being string of S st b1 = <*l*> ^ phi holds
b1 is 1 + (Depth phi) -wff
proofend;
end;

Lm32:  for S being Language
for U being non empty set
for I being Relation st I in U -InterpretersOf S holds
dom I = OwnSymbolsOf S
proofend;

registration
let S be Language;
let U be non empty set ;
cluster  ->  OwnSymbolsOf S -defined for Element of U -InterpretersOf S;
coherence
 for b1 being Element of U -InterpretersOf S holds b1 is OwnSymbolsOf S -defined
proofend;
end;

registration
let S be Language;
let U be non empty set ;
cluster Relation-like OwnSymbolsOf S -defined Function-like Function-yielding V164() S,U -interpreter-like for Element of U -InterpretersOf S;
existence
 ex b1 being Element of U -InterpretersOf S st b1 is OwnSymbolsOf S -defined
proofend;
end;

registration
let S be Language;
let U be non empty set ;
cluster OwnSymbolsOf S -defined  ->  OwnSymbolsOf S -defined total for Element of U -InterpretersOf S;
coherence
 for b1 being OwnSymbolsOf S -defined Element of U -InterpretersOf S holds b1 is total
proofend;
end;

definition
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let x be literal Element of S;
let u be Element of U;
:: original:ReassignIn
redefine func(x,u) ReassignIn I ->  Element of U -InterpretersOf S;
coherence
 (x,u) ReassignIn I is Element of U -InterpretersOf S
proofend;
end;

Lm33:  for m being Nat
for S being Language
for w being string of S
for U being non empty set
for I being Element of U -InterpretersOf S st w is m -wff holds
((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]
proofend;

Lm34:  for m being Nat
for S being Language
for U being non empty set
for l being literal Element of S
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] &amp; phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
proofend;

Lm35:  for S being Language
for U being non empty set
for l being literal Element of S
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
proofend;

Lm36:  for m being Nat
for S being Language
for w2 being string of S
for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] &amp; phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 &amp; f . (I,w2) = 0 ) )
proofend;

Lm37:  for S being Language
for U being non empty set
for phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE &amp; I -TruthEval phi2 = FALSE ) )
proofend;

definition
let S be Language;
let w be string of S;
func xnot w ->  string of S equals :: FOMODEL2:def 33
(<*(TheNorSymbOf S)*> ^ w) ^ w;
coherence
 (<*(TheNorSymbOf S)*> ^ w) ^ w is string of S ;
end;

:: deftheorem  defines xnot FOMODEL2:def_33_:_
 for S being Language
for w being string of S holds xnot w = (<*(TheNorSymbOf S)*> ^ w) ^ w;

registration
let S be Language;
let m be Nat;
let phi be m -wff string of S;
cluster xnot phi -> m + 1 -wff for string of S;
coherence
 for b1 being string of S st b1 = xnot phi holds
b1 is m + 1 -wff ;
end;

registration
let S be Language;
let phi be wff string of S;
cluster xnot phi ->  wff for string of S;
coherence
 for b1 being string of S st b1 = xnot phi holds
b1 is wff ;
end;

registration
let S be Language;
cluster TheEqSymbOf S ->  non own for Element of S;
coherence
 for b1 being Element of S st b1 = TheEqSymbOf S holds
not b1 is own
proofend;
end;

definition
let S be Language;
let X be set ;
attrX is S -mincover  means :Def34: :: FOMODEL2:def 34
 for phi being wff string of S holds
( phi in X iff not xnot phi in X );
end;

:: deftheorem Def34 defines -mincover FOMODEL2:def_34_:_
 for S being Language
for X being set holds
( X is S -mincover iff for phi being wff string of S holds
( phi in X iff not xnot phi in X ) );

theorem Th17: :: FOMODEL2:17
for S being Language
for l being literal Element of S
for phi1, phi2 being wff string of S holds
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) &amp; Depth (<*l*> ^ phi1) = (Depth phi1) + 1 )
proofend;

theorem :: FOMODEL2:18
for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 holds
( ( phi is exal implies phi in m -ExFormulasOf S ) &amp; ( phi in m -ExFormulasOf S implies phi is exal ) &amp; ( not phi is exal implies phi in m -NorFormulasOf S ) &amp; ( phi in m -NorFormulasOf S implies not phi is exal ) ) by Lm27, Lm29;

theorem :: FOMODEL2:19
for S being Language
for U being non empty set
for l being literal Element of S
for phi, phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( ( I -TruthEval (<*l*> ^ phi) = TRUE implies ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 ) &amp; ( ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 implies I -TruthEval (<*l*> ^ phi) = TRUE ) &amp; ( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE implies ( I -TruthEval phi1 = FALSE &amp; I -TruthEval phi2 = FALSE ) ) &amp; ( I -TruthEval phi1 = FALSE &amp; I -TruthEval phi2 = FALSE implies I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE ) ) by Lm35, Lm37;

theorem Th20: :: FOMODEL2:20
for m being Nat
for S being Language
for U being non empty set
for u being Element of U
for I being b2,b3 -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)
proofend;

theorem Th21: :: FOMODEL2:21
for S being Language
for U being non empty set
for t being termal string of S
for I being b1,b2 -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))
proofend;

definition
let S be Language;
let phi be wff string of S;
set F = S -firstChar ;
set d = Depth phi;
set s = (S -firstChar) . phi;
set L = LettersOf S;
set N = TheNorSymbOf S;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
defpred S1[ set ] means  ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued &amp; $1 = [phi1,p] &amp; phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p );
func SubWffsOf phi ->  set  means :Def35: :: FOMODEL2:def 35
 ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued &amp; it = [phi1,p] &amp; phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) if  not phi is 0wff
otherwise it = [phi,{}];
existence
 ( ( not phi is 0wff implies ex b1 being set ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued &amp; b1 = [phi1,p] &amp; phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) &amp; ( phi is 0wff implies ex b1 being set st b1 = [phi,{}] ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( not phi is 0wff &amp; ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued &amp; b1 = [phi1,p] &amp; phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) &amp; ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued &amp; b2 = [phi1,p] &amp; phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) implies b1 = b2 ) &amp; ( phi is 0wff &amp; b1 = [phi,{}] &amp; b2 = [phi,{}] implies b1 = b2 ) )
proofend;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def35 defines SubWffsOf FOMODEL2:def_35_:_
 for S being Language
for phi being wff string of S
for b3 being set holds
( ( not phi is 0wff implies ( b3 = SubWffsOf phi iff ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued &amp; b3 = [phi1,p] &amp; phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) ) &amp; ( phi is 0wff implies ( b3 = SubWffsOf phi iff b3 = [phi,{}] ) ) );

definition
let S be Language;
let phi be wff string of S;
set IT = SubWffsOf phi;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
func head phi ->  wff string of S equals :: FOMODEL2:def 36
(SubWffsOf phi) `1 ;
coherence
 (SubWffsOf phi) `1 is wff string of S
proofend;
func tail phi ->  Element of (AllSymbolsOf S) *  equals :: FOMODEL2:def 37
(SubWffsOf phi) `2 ;
coherence
 (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) *
proofend;
end;

:: deftheorem  defines head FOMODEL2:def_36_:_
 for S being Language
for phi being wff string of S holds head phi = (SubWffsOf phi) `1 ;

:: deftheorem  defines tail FOMODEL2:def_37_:_
 for S being Language
for phi being wff string of S holds tail phi = (SubWffsOf phi) `2 ;

registration
let S be Language;
let m be Nat;
cluster(S -formulasOfMaxDepth m) \ (AllFormulasOf S) ->  empty for set ;
coherence
 for b1 being set st b1 = (S -formulasOfMaxDepth m) \ (AllFormulasOf S) holds
b1 is empty
proofend;
end;

registration
let S be Language;
cluster(AtomicFormulasOf S) \ (AllFormulasOf S) ->  empty for set ;
coherence
 for b1 being set st b1 = (AtomicFormulasOf S) \ (AllFormulasOf S) holds
b1 is empty
proofend;
end;

theorem :: FOMODEL2:22
for S being Language
for l being literal Element of S
for phi1, phi2 being wff string of S holds
( Depth (<*l*> ^ phi1) > Depth phi1 &amp; Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 &amp; Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 ) by Lm28, Lm30;

theorem Th23: :: FOMODEL2:23
for x being set
for S being Language
for p2 being FinSequence
for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi &amp; phi2 = head phi &amp; p2 = tail phi ) )
proofend;

registration
let S be Language;
let m1 be non zero Nat;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V199() non 0wff m1 -wff wff non exal for Element of ((AllSymbolsOf S) *) \ {{}};
existence
 not for b1 being non 0wff m1 -wff string of S holds b1 is exal
proofend;
end;

registration
let S be Language;
let phi be wff exal string of S;
cluster tail phi ->  empty for set ;
coherence
 for b1 being set st b1 = tail phi holds
b1 is empty
proofend;
end;

Lm38:  for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 &amp; not phi is exal holds
ex phi2 being b1 -wff string of S st tail phi = phi2
proofend;

definition
let S be Language;
let phi be non 0wff wff non exal string of S;
:: original:tail
redefine func tail phi ->  wff string of S;
coherence
 tail phi is wff string of S
proofend;
end;

registration
let S be Language;
let phi be non 0wff wff non exal string of S;
cluster tail phi ->  wff for string of S;
coherence
 for b1 being string of S st b1 = tail phi holds
b1 is wff ;
end;

registration
let S be Language;
let phi0 be 0wff string of S;
identify head phi0 with phi0 null ;
compatibility
 head phi0 = phi0 null
proofend;
end;

registration
let S be Language;
let phi be non 0wff wff non exal string of S;
cluster((S -firstChar) . phi) \+\ (TheNorSymbOf S) ->  empty for set ;
coherence
 for b1 being set st b1 = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds
b1 is empty
proofend;
end;

Lm39:  for m being Nat
for S being Language
for phi being wff string of S st not phi is 0wff &amp; not phi is exal &amp; phi is m + 1 -wff holds
( head phi is b1 -wff string of S &amp; tail phi is b1 -wff string of S )
proofend;

registration
let m be Nat;
let S be Language;
let phi be m + 1 -wff string of S;
cluster head phi -> m -wff for string of S;
coherence
 for b1 being string of S st b1 = head phi holds
b1 is m -wff
proofend;
end;

registration
let m be Nat;
let S be Language;
let phi be non 0wff m + 1 -wff non exal string of S;
cluster tail phi -> m -wff for string of S;
coherence
 for b1 being string of S st b1 = tail phi holds
b1 is m -wff by Lm39;
end;

theorem Th24: :: FOMODEL2:24
for m being Nat
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
proofend;

Lm40:  for S being Language
for U being non empty set
for phi0 being 0wff string of S
for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0
proofend;

registration
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let phi0 be 0wff string of S;
identifyI -TruthEval phi0 with I -AtomicEval phi0;
compatibility
 I -TruthEval phi0 = I -AtomicEval phi0 by Lm40;
identifyI -AtomicEval phi0 with I -TruthEval phi0;
compatibility
 I -AtomicEval phi0 = I -TruthEval phi0 ;
end;

registration
let S be Language;
cluster non literal ofAtomicFormula for Element of AllSymbolsOf S;
existence
 not for b1 being ofAtomicFormula Element of S holds b1 is literal
proofend;
end;

Lm41:  for X being set
for S being Language
for U being non empty set
for I1, I2 being b2,b3 -interpreter-like Function st I1 | X = I2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
proofend;

theorem :: FOMODEL2:25
for S being Language
for U being non empty set
for p being FinSequence
for u being Element of U
for l2 being literal Element of S
for I being b1,b2 -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
proofend;

definition
let X be set ;
let S be Language;
let s be Element of S;
attrs is X -occurring  means :Def38: :: FOMODEL2:def 38
s in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ X);
end;

:: deftheorem Def38 defines -occurring FOMODEL2:def_38_:_
 for X being set
for S being Language
for s being Element of S holds
( s is X -occurring iff s in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ X) );

definition
let S be Language;
let s be Element of S;
let X be set ;
attrX is s -containing  means :: FOMODEL2:def 39
s in SymbolsOf (((AllSymbolsOf S) *) \ ({{}} /\ X));
end;

:: deftheorem  defines -containing FOMODEL2:def_39_:_
 for S being Language
for s being Element of S
for X being set holds
( X is s -containing iff s in SymbolsOf (((AllSymbolsOf S) *) \ ({{}} /\ X)) );

notation
let X be set ;
let S be Language;
let s be Element of S;
antonym X -absent s for X -occurring ;
end;

notation
let S be Language;
let s be Element of S;
let X be set ;
antonym s -free X for s -containing ;
end;

registration
let X be finite set ;
let S be Language;
cluster literal non operational non relational termal own ofAtomicFormula X -absent for Element of AllSymbolsOf S;
existence
 ex b1 being literal Element of S st b1 is X -absent
proofend;
end;

Lm42:  for S being Language
for w being string of S st w is termal holds
(rng w) /\ (LettersOf S) <> {}
proofend;

registration
let S be Language;
let t be termal string of S;
cluster(rng t) /\ (LettersOf S) ->  non empty for set ;
coherence
 for b1 being set st b1 = (rng t) /\ (LettersOf S) holds
not b1 is empty by Lm42;
end;

Lm43:  for S being Language
for w being string of S st w is wff holds
(rng w) /\ (LettersOf S) <> {}
proofend;

registration
let S be Language;
let phi be wff string of S;
cluster(rng phi) /\ (LettersOf S) ->  non empty for set ;
coherence
 for b1 being set st b1 = (rng phi) /\ (LettersOf S) holds
not b1 is empty by Lm43;
end;

registration
let B be set ;
let S be Language;
let A be Subset of B;
clusterA -occurring  -> B -occurring for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is A -occurring holds
b1 is B -occurring
proofend;
end;

registration
let A, B be set ;
let S be Language;
clusterA null B -absent  -> A /\ B -absent for Element of AllSymbolsOf S;
coherence
 for b1 being Element of S st b1 is A null B -absent holds
b1 is A /\ B -absent ;
end;

registration
let F be finite set ;
let A be set ;
let S be Language;
clusterF -absent A -absent  -> F -absent A \/ F -absent for Element of AllSymbolsOf S;
coherence
 for b1 being F -absent Element of S st b1 is A -absent holds
b1 is A \/ F -absent
proofend;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster(OwnSymbolsOf S) \ (dom I) ->  empty for set ;
coherence
 for b1 being set st b1 = (OwnSymbolsOf S) \ (dom I) holds
b1 is empty
proofend;
end;

theorem :: FOMODEL2:26
for S being Language
for U being non empty set
for l being literal Element of S
for I being b1,b2 -interpreter-like Function ex u being Element of U st
( u = (I . l) . {} &amp; (l,u) ReassignIn I = I )
proofend;

definition
let S be Language;
let X be set ;
attrX is S -covering  means :: FOMODEL2:def 40
 for phi being wff string of S holds
( phi in X or xnot phi in X );
end;

:: deftheorem  defines -covering FOMODEL2:def_40_:_
 for S being Language
for X being set holds
( X is S -covering iff for phi being wff string of S holds
( phi in X or xnot phi in X ) );

registration
let S be Language;
clusterS -mincover  -> S -covering for set ;
coherence
 for b1 being set st b1 is S -mincover holds
b1 is S -covering
proofend;
end;

registration
let U be non empty set ;
let S be Language;
let phi be non 0wff wff non exal string of S;
let I be Element of U -InterpretersOf S;
cluster(I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) ->  empty for set ;
coherence
 for b1 being set st b1 = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds
b1 is empty
proofend;
end;

definition
let S be Language;
func ExFormulasOf S ->  Subset of (((AllSymbolsOf S) *) \ {{}}) equals :: FOMODEL2:def 41
 {  phi where phi is string of S : ( phi is wff &amp; phi is exal )  }  ;
coherence
  {  phi where phi is string of S : ( phi is wff &amp; phi is exal )  }  is Subset of (((AllSymbolsOf S) *) \ {{}})
proofend;
end;

:: deftheorem  defines ExFormulasOf FOMODEL2:def_41_:_
 for S being Language holds ExFormulasOf S =  {  phi where phi is string of S : ( phi is wff &amp; phi is exal )  }  ;

registration
let S be Language;
cluster ExFormulasOf S ->  non empty for set ;
coherence
 for b1 being set st b1 = ExFormulasOf S holds
not b1 is empty
proofend;
end;

registration
let S be Language;
cluster  ->  wff exal for Element of ExFormulasOf S;
coherence
 for b1 being Element of ExFormulasOf S holds
( b1 is exal &amp; b1 is wff )
proofend;
end;

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

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

registration
let S be Language;
cluster(ExFormulasOf S) \ (AllFormulasOf S) ->  empty for set ;
coherence
 for b1 being set st b1 = (ExFormulasOf S) \ (AllFormulasOf S) holds
b1 is empty
proofend;
end;

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
cluster Relation-like Function-like S2,U -interpreter-like  -> S1,U -interpreter-like for set ;
coherence
 for b1 being Function st b1 is S2,U -interpreter-like holds
b1 is S1,U -interpreter-like
proofend;
end;

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
let I be S2,U -interpreter-like Function;
clusterI | (OwnSymbolsOf S1) -> S1,U -interpreter-like for Function;
coherence
 for b1 being Function st b1 = I | (OwnSymbolsOf S1) holds
b1 is S1,U -interpreter-like ;
end;

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
let I1 be Element of U -InterpretersOf S1;
let I2 be S2,U -interpreter-like Function;
clusterI2 +* I1 -> S2,U -interpreter-like ;
coherence
 I2 +* I1 is S2,U -interpreter-like
proofend;
end;

definition
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X be set ;
attrX is I -satisfied  means :Def42: :: FOMODEL2:def 42
 for phi being wff string of S st phi in X holds
I -TruthEval phi = 1;
end;

:: deftheorem Def42 defines -satisfied FOMODEL2:def_42_:_
 for U being non empty set
for S being Language
for I being Element of U -InterpretersOf S
for X being set holds
( X is I -satisfied iff for phi being wff string of S st phi in X holds
I -TruthEval phi = 1 );

definition
let S be Language;
let U be non empty set ;
let X be set ;
let I be Element of U -InterpretersOf S;
attrI is X -satisfying  means :Def43: :: FOMODEL2:def 43
X is I -satisfied ;
end;

:: deftheorem Def43 defines -satisfying FOMODEL2:def_43_:_
 for S being Language
for U being non empty set
for X being set
for I being Element of U -InterpretersOf S holds
( I is X -satisfying iff X is I -satisfied );

registration
let U be non empty set ;
let S be Language;
let e be empty set ;
let I be Element of U -InterpretersOf S;
clustere null I -> I -satisfied ;
coherence
 e null I is I -satisfied
proofend;
end;

registration
let X be set ;
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
clusterI -satisfied for Element of bool X;
existence
 ex b1 being Subset of X st b1 is I -satisfied
proofend;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
clusterI -satisfied for set ;
existence
 ex b1 being set st b1 is I -satisfied
proofend;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X be I -satisfied set ;
cluster  -> I -satisfied for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is I -satisfied
proofend;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X, Y be I -satisfied set ;
clusterX \/ Y -> I -satisfied ;
coherence
 X \/ Y is I -satisfied
proofend;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X be I -satisfied set ;
clusterI null X -> X -satisfying for Element of U -InterpretersOf S;
coherence
 for b1 being Element of U -InterpretersOf S st b1 = I null X holds
b1 is X -satisfying by Def43;
end;

definition
let S be Language;
let X be set ;
attrX is S -correct  means :Def44: :: FOMODEL2:def 44
 for U being non empty set
for I being Element of U -InterpretersOf S
for x being b2 -satisfied set
for phi being wff string of S st [x,phi] in X holds
I -TruthEval phi = 1;
end;

:: deftheorem Def44 defines -correct FOMODEL2:def_44_:_
 for S being Language
for X being set holds
( X is S -correct iff for U being non empty set
for I being Element of U -InterpretersOf S
for x being b4 -satisfied set
for phi being wff string of S st [x,phi] in X holds
I -TruthEval phi = 1 );

registration
let S be Language;
cluster{} null S -> S -correct ;
coherence
 {} null S is S -correct
proofend;
end;

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

theorem :: FOMODEL2:27
for S being Language
for U being non empty set
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval phi = 1 iff {phi} is I -satisfied )
proofend;

theorem :: FOMODEL2:28
for S being Language
for s being Element of S
for w being string of S holds
( s is {w} -occurring iff s in rng w )
proofend;

registration
let U be non empty set ;
let S be Language;
let phi1, phi2 be wff string of S;
let I be Element of U -InterpretersOf S;
cluster(I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) ->  empty for set ;
coherence
 for b1 being set st b1 = (I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) holds
b1 is empty
proofend;
end;

registration
let S be Language;
let phi be wff string of S;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
cluster(I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) ->  empty for set ;
coherence
 for b1 being set st b1 = (I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) holds
b1 is empty
proofend;
end;

definition
let X be set ;
let S be Language;
let phi be wff string of S;
attrphi is X -implied  means :: FOMODEL2:def 45
 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  defines -implied FOMODEL2:def_45_:_
 for X being set
for S being Language
for phi being wff string of S holds
( phi is X -implied iff for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1 );