let n be Nat; :: thesis: for s being set

for S1, S2 being BoolSignature st the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct holds

S2 is bool-correct

let s be set ; :: thesis: for S1, S2 being BoolSignature st the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct holds

S2 is bool-correct

let S1, S2 be BoolSignature ; :: thesis: ( the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct implies S2 is bool-correct )

assume A1: the bool-sort of S1 = the bool-sort of S2 ; :: thesis: ( not len the connectives of S2 >= 3 or ex i being Nat st

( i >= 1 & i <= 3 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is bool-correct or S2 is bool-correct )

assume A2: len the connectives of S2 >= 3 ; :: thesis: ( ex i being Nat st

( i >= 1 & i <= 3 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is bool-correct or S2 is bool-correct )

assume A3: for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ; :: thesis: ( not S1 is bool-correct or S2 is bool-correct )

set B = S1;

assume A4: ( len the connectives of S1 >= 3 & the connectives of S1 . 1 is_of_type {} , the bool-sort of S1 & the connectives of S1 . 2 is_of_type <* the bool-sort of S1*>, the bool-sort of S1 & the connectives of S1 . 3 is_of_type <* the bool-sort of S1, the bool-sort of S1*>, the bool-sort of S1 ) ; :: according to AOFA_A00:def 30 :: thesis: S2 is bool-correct

thus len the connectives of S2 >= 3 by A2; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of S2 . 1 is_of_type {} , the bool-sort of S2 & the connectives of S2 . 2 is_of_type <* the bool-sort of S2*>, the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the Arity of S2 . ( the connectives of S2 . 1) = the Arity of S1 . ( the connectives of S1 . 1) by A3

.= {} by A4 ; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . 1) = the bool-sort of S2 & the connectives of S2 . 2 is_of_type <* the bool-sort of S2*>, the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . 1) = the ResultSort of S1 . ( the connectives of S1 . 1) by A3

.= the bool-sort of S2 by A1, A4 ; :: thesis: ( the connectives of S2 . 2 is_of_type <* the bool-sort of S2*>, the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the Arity of S2 . ( the connectives of S2 . 2) = the Arity of S1 . ( the connectives of S1 . 2) by A3

.= <* the bool-sort of S2*> by A1, A4 ; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . 2) = the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . 2) = the ResultSort of S1 . ( the connectives of S1 . 2) by A3

.= the bool-sort of S2 by A1, A4 ; :: thesis: the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2

thus the Arity of S2 . ( the connectives of S2 . 3) = the Arity of S1 . ( the connectives of S1 . 3) by A3

.= <* the bool-sort of S2, the bool-sort of S2*> by A1, A4 ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of S2 . ( the connectives of S2 . 3) = the bool-sort of S2

thus the ResultSort of S2 . ( the connectives of S2 . 3) = the ResultSort of S1 . ( the connectives of S1 . 3) by A3

.= the bool-sort of S2 by A1, A4 ; :: thesis: verum

for S1, S2 being BoolSignature st the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct holds

S2 is bool-correct

let s be set ; :: thesis: for S1, S2 being BoolSignature st the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct holds

S2 is bool-correct

let S1, S2 be BoolSignature ; :: thesis: ( the bool-sort of S1 = the bool-sort of S2 & len the connectives of S2 >= 3 & ( for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) & S1 is bool-correct implies S2 is bool-correct )

assume A1: the bool-sort of S1 = the bool-sort of S2 ; :: thesis: ( not len the connectives of S2 >= 3 or ex i being Nat st

( i >= 1 & i <= 3 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is bool-correct or S2 is bool-correct )

assume A2: len the connectives of S2 >= 3 ; :: thesis: ( ex i being Nat st

( i >= 1 & i <= 3 & not ( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ) or not S1 is bool-correct or S2 is bool-correct )

assume A3: for i being Nat st i >= 1 & i <= 3 holds

( the Arity of S1 . ( the connectives of S1 . i) = the Arity of S2 . ( the connectives of S2 . i) & the ResultSort of S1 . ( the connectives of S1 . i) = the ResultSort of S2 . ( the connectives of S2 . i) ) ; :: thesis: ( not S1 is bool-correct or S2 is bool-correct )

set B = S1;

assume A4: ( len the connectives of S1 >= 3 & the connectives of S1 . 1 is_of_type {} , the bool-sort of S1 & the connectives of S1 . 2 is_of_type <* the bool-sort of S1*>, the bool-sort of S1 & the connectives of S1 . 3 is_of_type <* the bool-sort of S1, the bool-sort of S1*>, the bool-sort of S1 ) ; :: according to AOFA_A00:def 30 :: thesis: S2 is bool-correct

thus len the connectives of S2 >= 3 by A2; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of S2 . 1 is_of_type {} , the bool-sort of S2 & the connectives of S2 . 2 is_of_type <* the bool-sort of S2*>, the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the Arity of S2 . ( the connectives of S2 . 1) = the Arity of S1 . ( the connectives of S1 . 1) by A3

.= {} by A4 ; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . 1) = the bool-sort of S2 & the connectives of S2 . 2 is_of_type <* the bool-sort of S2*>, the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . 1) = the ResultSort of S1 . ( the connectives of S1 . 1) by A3

.= the bool-sort of S2 by A1, A4 ; :: thesis: ( the connectives of S2 . 2 is_of_type <* the bool-sort of S2*>, the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the Arity of S2 . ( the connectives of S2 . 2) = the Arity of S1 . ( the connectives of S1 . 2) by A3

.= <* the bool-sort of S2*> by A1, A4 ; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of S2 . ( the connectives of S2 . 2) = the bool-sort of S2 & the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2 )

thus the ResultSort of S2 . ( the connectives of S2 . 2) = the ResultSort of S1 . ( the connectives of S1 . 2) by A3

.= the bool-sort of S2 by A1, A4 ; :: thesis: the connectives of S2 . 3 is_of_type <* the bool-sort of S2, the bool-sort of S2*>, the bool-sort of S2

thus the Arity of S2 . ( the connectives of S2 . 3) = the Arity of S1 . ( the connectives of S1 . 3) by A3

.= <* the bool-sort of S2, the bool-sort of S2*> by A1, A4 ; :: according to AOFA_A00:def 8 :: thesis: the ResultSort of S2 . ( the connectives of S2 . 3) = the bool-sort of S2

thus the ResultSort of S2 . ( the connectives of S2 . 3) = the ResultSort of S1 . ( the connectives of S1 . 3) by A3

.= the bool-sort of S2 by A1, A4 ; :: thesis: verum