:: Grzegorczyk's Logics, Part 1
:: by Taneli Huuskonen
::
:: Received April 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


::
:: The Construction of Grzegorczyk's LD Language
::
definition
func VAR -> FinSequence-membered set equals :: GRZLOG_1:def 1
 { <*0,k*> where k is Element of NAT : verum } ;
coherence
{ <*0,k*> where k is Element of NAT : verum } is FinSequence-membered set
proof end;
end;

:: deftheorem defines VAR GRZLOG_1:def 1 :
VAR = { <*0,k*> where k is Element of NAT : verum } ;

registration
cluster VAR -> non empty FinSequence-membered antichain-like ;
coherence
( not VAR is empty & VAR is antichain-like )
proof end;
end;

definition
mode Variable is Element of VAR ;
end;

Lm1: for a being Variable holds a . 1 = 0
proof end;

definition
func 'not' -> FinSequence equals :: GRZLOG_1:def 2
<*1*>;
coherence
<*1*> is FinSequence ;
func '&' -> FinSequence equals :: GRZLOG_1:def 3
<*2*>;
coherence
<*2*> is FinSequence ;
func '=' -> FinSequence equals :: GRZLOG_1:def 4
<*3*>;
coherence
<*3*> is FinSequence ;
end;

:: deftheorem defines 'not' GRZLOG_1:def 2 :
'not' = <*1*>;

:: deftheorem defines '&' GRZLOG_1:def 3 :
'&' = <*2*>;

:: deftheorem defines '=' GRZLOG_1:def 4 :
'=' = <*3*>;

definition
func GRZ-ops -> non empty FinSequence-membered set equals :: GRZLOG_1:def 5
{'not','&','='};
coherence
{'not','&','='} is non empty FinSequence-membered set
proof end;
end;

:: deftheorem defines GRZ-ops GRZLOG_1:def 5 :
GRZ-ops = {'not','&','='};

Lm2: for p being Element of GRZ-ops holds
( dom p = Seg 1 & p . 1 <> 0 )
proof end;

definition
:: original: GRZ-ops
redefine func GRZ-ops -> Polish-language;
coherence
GRZ-ops is Polish-language
proof end;
end;

definition
func GRZ-symbols -> non empty FinSequence-membered set equals :: GRZLOG_1:def 6
VAR \/ GRZ-ops;
coherence
VAR \/ GRZ-ops is non empty FinSequence-membered set
proof end;
end;

:: deftheorem defines GRZ-symbols GRZLOG_1:def 6 :
GRZ-symbols = VAR \/ GRZ-ops;

definition
:: original: 'not'
redefine func 'not' -> Element of GRZ-symbols ;
coherence
'not' is Element of GRZ-symbols
proof end;
:: original: '&'
redefine func '&' -> Element of GRZ-symbols ;
coherence
'&' is Element of GRZ-symbols
proof end;
:: original: '='
redefine func '=' -> Element of GRZ-symbols ;
coherence
'=' is Element of GRZ-symbols
proof end;
end;

Lm3: for p being Element of GRZ-symbols holds
( p . 1 = 0 iff p in VAR )
proof end;

Lm4: for a being object holds
( not a in VAR or not a in GRZ-ops )
proof end;

theorem Th1: :: GRZLOG_1:1
( 'not' <> '&' & 'not' <> '=' & '&' <> '=' )
proof end;

Th3: ( not GRZ-symbols is trivial & GRZ-symbols is antichain-like )
proof end;

registration
cluster GRZ-symbols -> non empty non trivial FinSequence-membered antichain-like ;
coherence
( not GRZ-symbols is trivial & GRZ-symbols is antichain-like ) by Th3;
end;

definition
func GRZ-op-arity -> Function of GRZ-ops,NAT means :Def3: :: GRZLOG_1:def 7
( it . 'not' = 1 & it . '&' = 2 & it . '=' = 2 );
existence
ex b1 being Function of GRZ-ops,NAT st
( b1 . 'not' = 1 & b1 . '&' = 2 & b1 . '=' = 2 )
proof end;
uniqueness
for b1, b2 being Function of GRZ-ops,NAT st b1 . 'not' = 1 & b1 . '&' = 2 & b1 . '=' = 2 & b2 . 'not' = 1 & b2 . '&' = 2 & b2 . '=' = 2 holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines GRZ-op-arity GRZLOG_1:def 7 :
for b1 being Function of GRZ-ops,NAT holds
( b1 = GRZ-op-arity iff ( b1 . 'not' = 1 & b1 . '&' = 2 & b1 . '=' = 2 ) );

definition
func GRZ-arity -> Polish-arity-function of GRZ-symbols means :Def4: :: GRZLOG_1:def 8
 for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies it . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies it . a = 0 ) );
existence
ex b1 being Polish-arity-function of GRZ-symbols st
for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies b1 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b1 . a = 0 ) )
proof end;
uniqueness
for b1, b2 being Polish-arity-function of GRZ-symbols st ( for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies b1 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b1 . a = 0 ) ) ) & ( for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies b2 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b2 . a = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines GRZ-arity GRZLOG_1:def 8 :
for b1 being Polish-arity-function of GRZ-symbols holds
( b1 = GRZ-arity iff for a being object st a in GRZ-symbols holds
( ( a in GRZ-ops implies b1 . a = GRZ-op-arity . a ) & ( not a in GRZ-ops implies b1 . a = 0 ) ) );

Lm10: for a being object st a in GRZ-ops holds
GRZ-arity . a = GRZ-op-arity . a
proof end;

theorem Th4: :: GRZLOG_1:2
( GRZ-arity . 'not' = 1 & GRZ-arity . '&' = 2 & GRZ-arity . '=' = 2 )
proof end;

theorem Th5: :: GRZLOG_1:3
Polish-atoms (GRZ-symbols,GRZ-arity) = VAR
proof end;

definition
func GRZ-formula-set -> Polish-language of GRZ-symbols equals :: GRZLOG_1:def 9
 Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
Polish-WFF-set (GRZ-symbols,GRZ-arity) is Polish-language of GRZ-symbols ;
mode GRZ-formula is Polish-WFF of GRZ-symbols,GRZ-arity;
end;

:: deftheorem defines GRZ-formula-set GRZLOG_1:def 9 :
GRZ-formula-set = Polish-WFF-set (GRZ-symbols,GRZ-arity);

registration
cluster non empty functional FinSequence-membered for Element of bool GRZ-formula-set;
existence
not for b1 being Subset of GRZ-formula-set holds b1 is empty
proof end;
end;

definition
let n be Element of NAT ;
func x. n -> GRZ-formula equals :: GRZLOG_1:def 10
<*0,n*>;
coherence
<*0,n*> is GRZ-formula
proof end;
end;

:: deftheorem defines x. GRZLOG_1:def 10 :
for n being Element of NAT holds x. n = <*0,n*>;

definition
let t be GRZ-formula;
func 'not' t -> GRZ-formula equals :: GRZLOG_1:def 11
(Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;
coherence
(Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t is GRZ-formula ;
let u be GRZ-formula;
func t '&' u -> GRZ-formula equals :: GRZLOG_1:def 12
(Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);
coherence
(Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u) is GRZ-formula ;
func t '=' u -> GRZ-formula equals :: GRZLOG_1:def 13
(Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u);
coherence
(Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u) is GRZ-formula ;
end;

:: deftheorem defines 'not' GRZLOG_1:def 11 :
for t being GRZ-formula holds 'not' t = (Polish-unOp (GRZ-symbols,GRZ-arity,'not')) . t;

:: deftheorem defines '&' GRZLOG_1:def 12 :
for t, u being GRZ-formula holds t '&' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);

:: deftheorem defines '=' GRZLOG_1:def 13 :
for t, u being GRZ-formula holds t '=' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (t,u);

definition
let t, u be GRZ-formula;
func t 'or' u -> GRZ-formula equals :: GRZLOG_1:def 14
 'not' (('not' t) '&' ('not' u));
coherence
'not' (('not' t) '&' ('not' u)) is GRZ-formula ;
func t => u -> GRZ-formula equals :: GRZLOG_1:def 15
t '=' (t '&' u);
coherence
t '=' (t '&' u) is GRZ-formula ;
end;

:: deftheorem defines 'or' GRZLOG_1:def 14 :
for t, u being GRZ-formula holds t 'or' u = 'not' (('not' t) '&' ('not' u));

:: deftheorem defines => GRZLOG_1:def 15 :
for t, u being GRZ-formula holds t => u = t '=' (t '&' u);

definition
let t, u be GRZ-formula;
func t <=> u -> GRZ-formula equals :: GRZLOG_1:def 16
(t => u) '&' (u => t);
coherence
(t => u) '&' (u => t) is GRZ-formula ;
end;

:: deftheorem defines <=> GRZLOG_1:def 16 :
for t, u being GRZ-formula holds t <=> u = (t => u) '&' (u => t);

definition
let t be GRZ-formula;
attr t is atomic means :: GRZLOG_1:def 17
t in Polish-atoms (GRZ-symbols,GRZ-arity);
attr t is negative means :: GRZLOG_1:def 18
 Polish-WFF-head t = 'not' ;
attr t is conjunctive means :: GRZLOG_1:def 19
 Polish-WFF-head t = '&' ;
attr t is being_equality means :: GRZLOG_1:def 20
 Polish-WFF-head t = '=' ;
end;

:: deftheorem defines atomic GRZLOG_1:def 17 :
for t being GRZ-formula holds
( t is atomic iff t in Polish-atoms (GRZ-symbols,GRZ-arity) );

:: deftheorem defines negative GRZLOG_1:def 18 :
for t being GRZ-formula holds
( t is negative iff Polish-WFF-head t = 'not' );

:: deftheorem defines conjunctive GRZLOG_1:def 19 :
for t being GRZ-formula holds
( t is conjunctive iff Polish-WFF-head t = '&' );

:: deftheorem defines being_equality GRZLOG_1:def 20 :
for t being GRZ-formula holds
( t is being_equality iff Polish-WFF-head t = '=' );

theorem :: GRZLOG_1:4
for t being GRZ-formula holds
( t is atomic iff t in VAR ) by Th5;

theorem :: GRZLOG_1:5
for t being GRZ-formula holds
( t is negative iff ex u being GRZ-formula st t = 'not' u )
proof end;

theorem :: GRZLOG_1:6
for t being GRZ-formula holds
( t is conjunctive iff ex u, v being GRZ-formula st t = u '&' v )
proof end;

theorem :: GRZLOG_1:7
for t being GRZ-formula holds
( t is being_equality iff ex u, v being GRZ-formula st t = u '=' v )
proof end;

theorem :: GRZLOG_1:8
for t being GRZ-formula holds
( t is atomic or t is negative or t is conjunctive or t is being_equality )
proof end;

registration
cluster atomic -> non negative for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is atomic holds
not b1 is negative
proof end;
cluster atomic -> non conjunctive for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is atomic holds
not b1 is conjunctive
proof end;
cluster atomic -> non being_equality for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is atomic holds
not b1 is being_equality
proof end;
cluster negative -> non conjunctive for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is negative holds
not b1 is conjunctive by Th1;
cluster negative -> non being_equality for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is negative holds
not b1 is being_equality by Th1;
cluster conjunctive -> non being_equality for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is conjunctive holds
not b1 is being_equality by Th1;
end;

definition
func GRZ-axioms -> non empty Subset of GRZ-formula-set means :Def10: :: GRZLOG_1:def 21
 for a being object holds
( a in it iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) );
existence
ex b1 being non empty Subset of GRZ-formula-set st
for a being object holds
( a in b1 iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) )
proof end;
uniqueness
for b1, b2 being non empty Subset of GRZ-formula-set st ( for a being object holds
( a in b1 iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) ) ) & ( for a being object holds
( a in b2 iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) ) ) holds
b1 = b2
proof end;
func LD-specific-axioms -> non empty Subset of GRZ-formula-set means :Def11: :: GRZLOG_1:def 22
 for a being object holds
( a in it iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) );
existence
ex b1 being non empty Subset of GRZ-formula-set st
for a being object holds
( a in b1 iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) )
proof end;
uniqueness
for b1, b2 being non empty Subset of GRZ-formula-set st ( for a being object holds
( a in b1 iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) ) ) & ( for a being object holds
( a in b2 iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines GRZ-axioms GRZLOG_1:def 21 :
for b1 being non empty Subset of GRZ-formula-set holds
( b1 = GRZ-axioms iff for a being object holds
( a in b1 iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) ) );

:: deftheorem Def11 defines LD-specific-axioms GRZLOG_1:def 22 :
for b1 being non empty Subset of GRZ-formula-set holds
( b1 = LD-specific-axioms iff for a being object holds
( a in b1 iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) ) );

definition
func LD-axioms -> non empty Subset of GRZ-formula-set equals :: GRZLOG_1:def 23
GRZ-axioms \/ LD-specific-axioms;
coherence
GRZ-axioms \/ LD-specific-axioms is non empty Subset of GRZ-formula-set ;
end;

:: deftheorem defines LD-axioms GRZLOG_1:def 23 :
LD-axioms = GRZ-axioms \/ LD-specific-axioms;

definition
mode GRZ-rule is Relation of (bool GRZ-formula-set),GRZ-formula-set;
end;

definition
let R1, R2 be GRZ-rule;
:: original: \/
redefine func R1 \/ R2 -> GRZ-rule;
coherence
R1 \/ R2 is GRZ-rule by XBOOLE_1:8;
end;

definition
func GRZ-MP -> GRZ-rule equals :: GRZLOG_1:def 24
 { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;
coherence
{ [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule
proof end;
func GRZ-ConjIntro -> GRZ-rule equals :: GRZLOG_1:def 25
 { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;
coherence
{ [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } is GRZ-rule
proof end;
func GRZ-ConjElimL -> GRZ-rule equals :: GRZLOG_1:def 26
 { [{(t '&' u)},t] where t, u is GRZ-formula : verum } ;
coherence
{ [{(t '&' u)},t] where t, u is GRZ-formula : verum } is GRZ-rule
proof end;
func GRZ-ConjElimR -> GRZ-rule equals :: GRZLOG_1:def 27
 { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;
coherence
{ [{(t '&' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule
proof end;
end;

:: deftheorem defines GRZ-MP GRZLOG_1:def 24 :
GRZ-MP = { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;

:: deftheorem defines GRZ-ConjIntro GRZLOG_1:def 25 :
GRZ-ConjIntro = { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;

:: deftheorem defines GRZ-ConjElimL GRZLOG_1:def 26 :
GRZ-ConjElimL = { [{(t '&' u)},t] where t, u is GRZ-formula : verum } ;

:: deftheorem defines GRZ-ConjElimR GRZLOG_1:def 27 :
GRZ-ConjElimR = { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;

definition
func GRZ-rules -> GRZ-rule means :Def35: :: GRZLOG_1:def 28
 for a being object holds
( a in it iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) );
existence
ex b1 being GRZ-rule st
for a being object holds
( a in b1 iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) )
proof end;
uniqueness
for b1, b2 being GRZ-rule st ( for a being object holds
( a in b1 iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) ) & ( for a being object holds
( a in b2 iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def35 defines GRZ-rules GRZLOG_1:def 28 :
for b1 being GRZ-rule holds
( b1 = GRZ-rules iff for a being object holds
( a in b1 iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) );

definition
mode GRZ-formula-sequence is FinSequence of GRZ-formula-set ;
mode GRZ-formula-finset is finite Subset of GRZ-formula-set;
end;

definition
let S1, S2 be GRZ-formula-finset;
:: original: \/
redefine func S1 \/ S2 -> GRZ-formula-finset;
coherence
S1 \/ S2 is GRZ-formula-finset
proof end;
end;

definition
let A be non empty Subset of GRZ-formula-set;
let R be GRZ-rule;
let P be GRZ-formula-sequence;
let n be Element of NAT ;
pred P,n is_a_correct_step_wrt A,R means :: GRZLOG_1:def 29
( P . n in A or ex Q being GRZ-formula-finset st
( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds
ex k being Element of NAT st
( k in dom P & k < n & P . k = q ) ) ) );
end;

:: deftheorem defines is_a_correct_step_wrt GRZLOG_1:def 29 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P being GRZ-formula-sequence
for n being Element of NAT holds
( P,n is_a_correct_step_wrt A,R iff ( P . n in A or ex Q being GRZ-formula-finset st
( [Q,(P . n)] in R & ( for q being FinSequence st q in Q holds
ex k being Element of NAT st
( k in dom P & k < n & P . k = q ) ) ) ) );

definition
let A be non empty Subset of GRZ-formula-set;
let R be GRZ-rule;
let P be GRZ-formula-sequence;
attr P is A,R -correct means :: GRZLOG_1:def 30
 for k being Element of NAT st k in dom P holds
P,k is_a_correct_step_wrt A,R;
end;

:: deftheorem defines -correct GRZLOG_1:def 30 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P being GRZ-formula-sequence holds
( P is A,R -correct iff for k being Element of NAT st k in dom P holds
P,k is_a_correct_step_wrt A,R );

definition
let A be non empty Subset of GRZ-formula-set;
let a be Element of A;
:: original: <*
redefine func <*a*> -> GRZ-formula-sequence;
coherence
<*a*> is GRZ-formula-sequence
proof end;
end;

theorem Th40: :: GRZLOG_1:9
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for a being Element of A holds <*a*> is A,R -correct
proof end;

registration
let A be non empty Subset of GRZ-formula-set;
let R be GRZ-rule;
cluster V1() V4( NAT ) V5( GRZ-formula-set ) non empty Function-like finite FinSequence-like FinSubsequence-like A,R -correct for FinSequence of GRZ-formula-set ;
existence
ex b1 being GRZ-formula-sequence st
( not b1 is empty & b1 is A,R -correct )
proof end;
end;

definition
let A be non empty Subset of GRZ-formula-set;
let R be GRZ-rule;
let S be GRZ-formula-finset;
attr S is A,R -correct means :: GRZLOG_1:def 31
 ex P being GRZ-formula-sequence st
( S = rng P & P is A,R -correct );
end;

:: deftheorem defines -correct GRZLOG_1:def 31 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for S being GRZ-formula-finset holds
( S is A,R -correct iff ex P being GRZ-formula-sequence st
( S = rng P & P is A,R -correct ) );

Lm40: for p, q being FinSequence
for k, m being Element of NAT st k in dom p & m in dom q & m < k holds
m in dom p
proof end;

Lm41: for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P, P1, P2 being GRZ-formula-sequence
for n being Element of NAT st n in dom P & P ^ P1,n is_a_correct_step_wrt A,R holds
P ^ P2,n is_a_correct_step_wrt A,R
proof end;

theorem :: GRZLOG_1:10
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P, P1, P2 being GRZ-formula-sequence st P is A,R -correct & P = P1 ^ P2 holds
P1 is A,R -correct
proof end;

theorem Th42: :: GRZLOG_1:11
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for P1, P2 being GRZ-formula-sequence st P1 is A,R -correct & P2 is A,R -correct holds
P1 ^ P2 is A,R -correct
proof end;

theorem Th43: :: GRZLOG_1:12
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for S1, S2 being GRZ-formula-finset st S1 is A,R -correct & S2 is A,R -correct holds
S1 \/ S2 is A,R -correct
proof end;

Lm44: for A, A1 being non empty Subset of GRZ-formula-set
for R, R1 being GRZ-rule
for P being GRZ-formula-sequence
for k being Element of NAT st A c= A1 & R c= R1 & P,k is_a_correct_step_wrt A,R holds
P,k is_a_correct_step_wrt A1,R1
;

theorem Th44: :: GRZLOG_1:13
for A, A1 being non empty Subset of GRZ-formula-set
for R, R1 being GRZ-rule
for P being GRZ-formula-sequence st A c= A1 & R c= R1 & P is A,R -correct holds
P is A1,R1 -correct by Lm44;

definition
let A be non empty Subset of GRZ-formula-set;
let R be GRZ-rule;
let t be GRZ-formula;
pred A,R |- t means :: GRZLOG_1:def 32
 ex P being GRZ-formula-sequence st
( t in rng P & P is A,R -correct );
end;

:: deftheorem defines |- GRZLOG_1:def 32 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for t being GRZ-formula holds
( A,R |- t iff ex P being GRZ-formula-sequence st
( t in rng P & P is A,R -correct ) );

definition
let A be non empty Subset of GRZ-formula-set;
let R be GRZ-rule;
let B be Subset of GRZ-formula-set;
pred A,R |- B means :: GRZLOG_1:def 33
 for t being GRZ-formula st t in B holds
A,R |- t;
end;

:: deftheorem defines |- GRZLOG_1:def 33 :
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for B being Subset of GRZ-formula-set holds
( A,R |- B iff for t being GRZ-formula st t in B holds
A,R |- t );

theorem Th45: :: GRZLOG_1:14
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for t being GRZ-formula holds
( A,R |- t iff ex S being GRZ-formula-finset st
( t in S & S is A,R -correct ) )
proof end;

theorem Th46: :: GRZLOG_1:15
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for t being GRZ-formula st t in A holds
A,R |- t
proof end;

theorem Th47: :: GRZLOG_1:16
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for S being GRZ-formula-finset st A,R |- S holds
ex S1 being GRZ-formula-finset st
( S c= S1 & S1 is A,R -correct )
proof end;

theorem Th48: :: GRZLOG_1:17
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for t being GRZ-formula
for S being GRZ-formula-finset st A,R |- S & [S,t] in R holds
A,R |- t
proof end;

theorem :: GRZLOG_1:18
for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for t being GRZ-formula holds
( not A,R |- t or t in A or ex S being GRZ-formula-finset st
( [S,t] in R & A,R |- S ) )
proof end;

theorem :: GRZLOG_1:19
for A, A1 being non empty Subset of GRZ-formula-set
for R, R1 being GRZ-rule
for t being GRZ-formula st A c= A1 & R c= R1 & A,R |- t holds
A1,R1 |- t by Th44;

theorem Th60: :: GRZLOG_1:20
for A being non empty Subset of GRZ-formula-set
for t, u being GRZ-formula holds
( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )
proof end;

theorem Th61: :: GRZLOG_1:21
for A being non empty Subset of GRZ-formula-set
for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u
proof end;

theorem Th62: :: GRZLOG_1:22
for A being non empty Subset of GRZ-formula-set
for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t => u holds
A, GRZ-rules |- u
proof end;

theorem :: GRZLOG_1:23
for A being non empty Subset of GRZ-formula-set
for t, u being GRZ-formula st A, GRZ-rules |- t '&' u holds
A, GRZ-rules |- u '&' t
proof end;

definition
let t be GRZ-formula;
attr t is GRZ-axiomatic means :: GRZLOG_1:def 34
t in GRZ-axioms ;
attr t is GRZ-provable means :: GRZLOG_1:def 35
 GRZ-axioms , GRZ-rules |- t;
attr t is LD-axiomatic means :: GRZLOG_1:def 36
t in LD-axioms ;
attr t is LD-provable means :: GRZLOG_1:def 37
 LD-axioms , GRZ-rules |- t;
end;

:: deftheorem defines GRZ-axiomatic GRZLOG_1:def 34 :
for t being GRZ-formula holds
( t is GRZ-axiomatic iff t in GRZ-axioms );

:: deftheorem defines GRZ-provable GRZLOG_1:def 35 :
for t being GRZ-formula holds
( t is GRZ-provable iff GRZ-axioms , GRZ-rules |- t );

:: deftheorem defines LD-axiomatic GRZLOG_1:def 36 :
for t being GRZ-formula holds
( t is LD-axiomatic iff t in LD-axioms );

:: deftheorem defines LD-provable GRZLOG_1:def 37 :
for t being GRZ-formula holds
( t is LD-provable iff LD-axioms , GRZ-rules |- t );

registration
let t be GRZ-formula;
cluster 'not' (t '&' ('not' t)) -> GRZ-axiomatic ;
coherence
'not' (t '&' ('not' t)) is GRZ-axiomatic by Def10;
cluster ('not' ('not' t)) '=' t -> GRZ-axiomatic ;
coherence
('not' ('not' t)) '=' t is GRZ-axiomatic by Def10;
cluster t '=' (t '&' t) -> GRZ-axiomatic ;
coherence
t '=' (t '&' t) is GRZ-axiomatic by Def10;
let u be GRZ-formula;
cluster (t '&' u) '=' (u '&' t) -> GRZ-axiomatic ;
coherence
(t '&' u) '=' (u '&' t) is GRZ-axiomatic by Def10;
cluster ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) -> GRZ-axiomatic ;
coherence
('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) is GRZ-axiomatic by Def10;
cluster (t '=' u) '=' (u '=' t) -> GRZ-axiomatic ;
coherence
(t '=' u) '=' (u '=' t) is GRZ-axiomatic by Def10;
cluster (t '=' u) '=' (('not' t) '=' ('not' u)) -> GRZ-axiomatic ;
coherence
(t '=' u) '=' (('not' t) '=' ('not' u)) is GRZ-axiomatic by Def10;
let v be GRZ-formula;
cluster (t '&' (u '&' v)) '=' ((t '&' u) '&' v) -> GRZ-axiomatic ;
coherence
(t '&' (u '&' v)) '=' ((t '&' u) '&' v) is GRZ-axiomatic by Def10;
cluster (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) -> GRZ-axiomatic ;
coherence
(t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) is GRZ-axiomatic by Def10;
cluster (t '=' u) => ((t '&' v) '=' (u '&' v)) -> LD-axiomatic ;
coherence
(t '=' u) => ((t '&' v) '=' (u '&' v)) is LD-axiomatic
proof end;
cluster (t '=' u) => ((t 'or' v) '=' (u 'or' v)) -> LD-axiomatic ;
coherence
(t '=' u) => ((t 'or' v) '=' (u 'or' v)) is LD-axiomatic
proof end;
cluster (t '=' u) => ((t '=' v) '=' (u '=' v)) -> LD-axiomatic ;
coherence
(t '=' u) => ((t '=' v) '=' (u '=' v)) is LD-axiomatic
proof end;
end;

registration
cluster GRZ-axiomatic -> LD-axiomatic for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is GRZ-axiomatic holds
b1 is LD-axiomatic by XBOOLE_0:def 3;
cluster GRZ-axiomatic -> GRZ-provable for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is GRZ-axiomatic holds
b1 is GRZ-provable by Th46;
cluster LD-axiomatic -> LD-provable for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is LD-axiomatic holds
b1 is LD-provable by Th46;
cluster GRZ-provable -> LD-provable for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
coherence
for b1 being GRZ-formula st b1 is GRZ-provable holds
b1 is LD-provable
proof end;
end;

registration
cluster V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like GRZ-axiomatic GRZ-provable LD-axiomatic LD-provable for Element of Polish-WFF-set (GRZ-symbols,GRZ-arity);
existence
ex b1 being GRZ-formula st
( b1 is GRZ-axiomatic & b1 is GRZ-provable & b1 is LD-axiomatic & b1 is LD-provable )
proof end;
end;

theorem Th70: :: GRZLOG_1:24
for A being non empty Subset of GRZ-formula-set
for t, u being GRZ-formula st GRZ-axioms c= A & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u '=' t
proof end;

theorem :: GRZLOG_1:25
for t, u being GRZ-formula st t '=' u is GRZ-provable holds
u '=' t is GRZ-provable by Th70;

theorem :: GRZLOG_1:26
for t, u being GRZ-formula st t '=' u is LD-provable holds
u '=' t is LD-provable by Th70, XBOOLE_1:7;

theorem Th74: :: GRZLOG_1:27
for t, u, v being GRZ-formula st t '=' u is LD-provable & u '=' v is LD-provable holds
t '=' v is LD-provable
proof end;

theorem Th75: :: GRZLOG_1:28
for t being GRZ-formula holds t '=' t is LD-provable
proof end;

definition
let t, u be GRZ-formula;
pred t LD-= u means :Def76: :: GRZLOG_1:def 38
t '=' u is LD-provable ;
reflexivity
for t being GRZ-formula holds t '=' t is LD-provable by Th75;
symmetry
for t, u being GRZ-formula st t '=' u is LD-provable holds
u '=' t is LD-provable by Th70, XBOOLE_1:7;
end;

:: deftheorem Def76 defines LD-= GRZLOG_1:def 38 :
for t, u being GRZ-formula holds
( t LD-= u iff t '=' u is LD-provable );

theorem Th76: :: GRZLOG_1:29
for t, u being GRZ-formula st t LD-= u holds
'not' t LD-= 'not' u
proof end;

scheme :: GRZLOG_1:sch 1
BinReplace{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> Element of F1(), P1[ Element of F1(), Element of F1()] } :
for a, b, c, d being Element of F1() st P1[a,b] & P1[c,d] holds
P1[F2(a,c),F2(b,d)]
provided
A2: for a, b, c being Element of F1() st P1[a,b] & P1[b,c] holds
P1[a,c] and
A3: for a, b being Element of F1() holds P1[F2(a,b),F2(b,a)] and
A4: for a, b, c being Element of F1() st P1[a,b] holds
P1[F2(a,c),F2(b,c)]
proof end;

Lm77a: for t, u, v being GRZ-formula st t '=' u is LD-provable holds
(t '&' v) '=' (u '&' v) is LD-provable
proof end;

theorem Th77: :: GRZLOG_1:30
for t, u, v, w being GRZ-formula st t LD-= u & v LD-= w holds
t '&' v LD-= u '&' w
proof end;

Lm78a: for t, u, v being GRZ-formula st t '=' u is LD-provable holds
(t '=' v) '=' (u '=' v) is LD-provable
proof end;

theorem Th78: :: GRZLOG_1:31
for t, u, v, w being GRZ-formula st t LD-= u & v LD-= w holds
t '=' v LD-= u '=' w
proof end;

definition
func LD-EqR -> Equivalence_Relation of GRZ-formula-set means :Def80: :: GRZLOG_1:def 39
 for t, u being GRZ-formula holds
( [t,u] in it iff t LD-= u );
existence
ex b1 being Equivalence_Relation of GRZ-formula-set st
for t, u being GRZ-formula holds
( [t,u] in b1 iff t LD-= u )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of GRZ-formula-set st ( for t, u being GRZ-formula holds
( [t,u] in b1 iff t LD-= u ) ) & ( for t, u being GRZ-formula holds
( [t,u] in b2 iff t LD-= u ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def80 defines LD-EqR GRZLOG_1:def 39 :
for b1 being Equivalence_Relation of GRZ-formula-set holds
( b1 = LD-EqR iff for t, u being GRZ-formula holds
( [t,u] in b1 iff t LD-= u ) );

registration
cluster non empty for Element of bool (bool GRZ-formula-set);
existence
not for b1 being Subset-Family of GRZ-formula-set holds b1 is empty
proof end;
end;

definition
func LD-EqClasses -> non empty Subset-Family of GRZ-formula-set equals :: GRZLOG_1:def 40
 Class LD-EqR;
coherence
Class LD-EqR is non empty Subset-Family of GRZ-formula-set ;
end;

:: deftheorem defines LD-EqClasses GRZLOG_1:def 40 :
LD-EqClasses = Class LD-EqR;

definition
mode LD-EqClass is Element of LD-EqClasses ;
end;

definition
let t be GRZ-formula;
func LD-EqClassOf t -> LD-EqClass equals :: GRZLOG_1:def 41
 Class (LD-EqR,t);
coherence
Class (LD-EqR,t) is LD-EqClass by EQREL_1:def 3;
end;

:: deftheorem defines LD-EqClassOf GRZLOG_1:def 41 :
for t being GRZ-formula holds LD-EqClassOf t = Class (LD-EqR,t);

theorem Th80: :: GRZLOG_1:32
for t, u being GRZ-formula holds
( t LD-= u iff LD-EqClassOf t = LD-EqClassOf u )
proof end;

scheme :: GRZLOG_1:sch 2
UnOpCongr{ F1() -> non empty set , F2( Element of F1()) -> Element of F1(), F3() -> Equivalence_Relation of F1() } :
ex f being UnOp of (Class F3()) st
for x being Element of F1() holds f . (Class (F3(),x)) = Class (F3(),F2(x))
provided
A1: for x, y being Element of F1() st [x,y] in F3() holds
[F2(x),F2(y)] in F3()
proof end;

scheme :: GRZLOG_1:sch 3
BinOpCongr{ F1() -> non empty set , F2( Element of F1(), Element of F1()) -> Element of F1(), F3() -> Equivalence_Relation of F1() } :
ex f being BinOp of (Class F3()) st
for x, y being Element of F1() holds f . ((Class (F3(),x)),(Class (F3(),y))) = Class (F3(),F2(x,y))
provided
A1: for x1, x2, y1, y2 being Element of F1() st [x1,x2] in F3() & [y1,y2] in F3() holds
[F2(x1,y1),F2(x2,y2)] in F3()
proof end;

theorem Th88: :: GRZLOG_1:33
for x being LD-EqClass ex t being GRZ-formula st x = LD-EqClassOf t
proof end;

definition
let x be LD-EqClass;
attr x is LD-provable means :: GRZLOG_1:def 42
 ex t being GRZ-formula st
( x = LD-EqClassOf t & t is LD-provable );
func 'not' x -> LD-EqClass means :Def91: :: GRZLOG_1:def 43
 ex t being GRZ-formula st
( x = LD-EqClassOf t & it = LD-EqClassOf ('not' t) );
existence
ex b1 being LD-EqClass ex t being GRZ-formula st
( x = LD-EqClassOf t & b1 = LD-EqClassOf ('not' t) )
proof end;
uniqueness
for b1, b2 being LD-EqClass st ex t being GRZ-formula st
( x = LD-EqClassOf t & b1 = LD-EqClassOf ('not' t) ) & ex t being GRZ-formula st
( x = LD-EqClassOf t & b2 = LD-EqClassOf ('not' t) ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being LD-EqClass st ex t being GRZ-formula st
( b2 = LD-EqClassOf t & b1 = LD-EqClassOf ('not' t) ) holds
ex t being GRZ-formula st
( b1 = LD-EqClassOf t & b2 = LD-EqClassOf ('not' t) )
proof end;
let y be LD-EqClass;
func x '&' y -> LD-EqClass means :Def92: :: GRZLOG_1:def 44
 ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & it = LD-EqClassOf (t '&' u) );
existence
ex b1 being LD-EqClass ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b1 = LD-EqClassOf (t '&' u) )
proof end;
uniqueness
for b1, b2 being LD-EqClass st ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b1 = LD-EqClassOf (t '&' u) ) & ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b2 = LD-EqClassOf (t '&' u) ) holds
b1 = b2
proof end;
commutativity
for b1, x, y being LD-EqClass st ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b1 = LD-EqClassOf (t '&' u) ) holds
ex t, u being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf u & b1 = LD-EqClassOf (t '&' u) )
proof end;
idempotence
for x being LD-EqClass ex t, u being GRZ-formula st
( x = LD-EqClassOf t & x = LD-EqClassOf u & x = LD-EqClassOf (t '&' u) )
proof end;
func x '=' y -> LD-EqClass means :Def93: :: GRZLOG_1:def 45
 ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & it = LD-EqClassOf (t '=' u) );
existence
ex b1 being LD-EqClass ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b1 = LD-EqClassOf (t '=' u) )
proof end;
uniqueness
for b1, b2 being LD-EqClass st ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b1 = LD-EqClassOf (t '=' u) ) & ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b2 = LD-EqClassOf (t '=' u) ) holds
b1 = b2
proof end;
commutativity
for b1, x, y being LD-EqClass st ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b1 = LD-EqClassOf (t '=' u) ) holds
ex t, u being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf u & b1 = LD-EqClassOf (t '=' u) )
proof end;
end;

:: deftheorem defines LD-provable GRZLOG_1:def 42 :
for x being LD-EqClass holds
( x is LD-provable iff ex t being GRZ-formula st
( x = LD-EqClassOf t & t is LD-provable ) );

:: deftheorem Def91 defines 'not' GRZLOG_1:def 43 :
for x, b2 being LD-EqClass holds
( b2 = 'not' x iff ex t being GRZ-formula st
( x = LD-EqClassOf t & b2 = LD-EqClassOf ('not' t) ) );

:: deftheorem Def92 defines '&' GRZLOG_1:def 44 :
for x, y, b3 being LD-EqClass holds
( b3 = x '&' y iff ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b3 = LD-EqClassOf (t '&' u) ) );

:: deftheorem Def93 defines '=' GRZLOG_1:def 45 :
for x, y, b3 being LD-EqClass holds
( b3 = x '=' y iff ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b3 = LD-EqClassOf (t '=' u) ) );

definition
let x, y be LD-EqClass;
func x 'or' y -> LD-EqClass equals :: GRZLOG_1:def 46
 'not' (('not' x) '&' ('not' y));
coherence
'not' (('not' x) '&' ('not' y)) is LD-EqClass ;
commutativity
for b1, x, y being LD-EqClass st b1 = 'not' (('not' x) '&' ('not' y)) holds
b1 = 'not' (('not' y) '&' ('not' x)) ;
idempotence
for x being LD-EqClass holds x = 'not' (('not' x) '&' ('not' x)) ;
func x => y -> LD-EqClass equals :: GRZLOG_1:def 47
x '=' (x '&' y);
coherence
x '=' (x '&' y) is LD-EqClass ;
end;

:: deftheorem defines 'or' GRZLOG_1:def 46 :
for x, y being LD-EqClass holds x 'or' y = 'not' (('not' x) '&' ('not' y));

:: deftheorem defines => GRZLOG_1:def 47 :
for x, y being LD-EqClass holds x => y = x '=' (x '&' y);

registration
let t be LD-provable GRZ-formula;
cluster LD-EqClassOf t -> LD-provable ;
coherence
LD-EqClassOf t is LD-provable ;
end;

theorem Th90: :: GRZLOG_1:34
for t being GRZ-formula st LD-EqClassOf t is LD-provable holds
t is LD-provable
proof end;

theorem Th91: :: GRZLOG_1:35
for x, y being LD-EqClass holds
( x '&' y is LD-provable iff ( x is LD-provable & y is LD-provable ) )
proof end;

theorem Th92: :: GRZLOG_1:36
for x, y being LD-EqClass holds
( x '=' y is LD-provable iff x = y )
proof end;

theorem :: GRZLOG_1:37
for t being GRZ-formula holds LD-EqClassOf ('not' t) = 'not' (LD-EqClassOf t) by Def91;

theorem :: GRZLOG_1:38
for t, u being GRZ-formula holds LD-EqClassOf (t '&' u) = (LD-EqClassOf t) '&' (LD-EqClassOf u) by Def92;

theorem :: GRZLOG_1:39
for t, u being GRZ-formula holds LD-EqClassOf (t '=' u) = (LD-EqClassOf t) '=' (LD-EqClassOf u) by Def93;

theorem Th96: :: GRZLOG_1:40
for t, u being GRZ-formula holds LD-EqClassOf (t 'or' u) = (LD-EqClassOf t) 'or' (LD-EqClassOf u)
proof end;

theorem Th97: :: GRZLOG_1:41
for t, u being GRZ-formula holds LD-EqClassOf (t => u) = (LD-EqClassOf t) => (LD-EqClassOf u)
proof end;

theorem Th98: :: GRZLOG_1:42
for x, y, z being LD-EqClass holds (x '&' y) '&' z = x '&' (y '&' z)
proof end;

theorem :: GRZLOG_1:43
for x, y being LD-EqClass holds
( x => y is LD-provable iff x = x '&' y ) by Th92;

theorem Th101: :: GRZLOG_1:44
for x, y, z being LD-EqClass st x => y is LD-provable & y => z is LD-provable holds
x => z is LD-provable
proof end;

theorem :: GRZLOG_1:45
for t, u, v being GRZ-formula st t => u is LD-provable & u => v is LD-provable holds
t => v is LD-provable
proof end;

theorem :: GRZLOG_1:46
for x, y, z being LD-EqClass holds x 'or' (y 'or' z) = (x 'or' y) 'or' z by Th98;

theorem Th104: :: GRZLOG_1:47
for x, y, z being LD-EqClass holds x '&' (y 'or' z) = (x '&' y) 'or' (x '&' z)
proof end;

theorem Th105: :: GRZLOG_1:48
for x, y, z being LD-EqClass holds x 'or' (y '&' z) = (x 'or' y) '&' (x 'or' z)
proof end;

theorem :: GRZLOG_1:49
for x, y being LD-EqClass holds
( ( x => y is LD-provable & y => x is LD-provable ) iff x = y )
proof end;

theorem :: GRZLOG_1:50
for x, y being LD-EqClass st x is LD-provable holds
x 'or' y is LD-provable
proof end;