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