let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let G be basic GeneratorSystem over S,X,T; :: thesis: for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let A be IfWhileAlgebra of the generators of G; :: thesis: for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let I be integer SortSymbol of S; :: thesis: for b being pure Element of the generators of G . the bool-sort of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let b be pure Element of the generators of G . the bool-sort of S; :: thesis: for t1, t2 being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let t1, t2 be Element of T,I; :: thesis: for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let s be Element of C -States the generators of G; :: thesis: for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( G is C -supported & f in C -Execution (A,b,(\false C)) implies ( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) ) )
assume A1: ( G is C -supported & f in C -Execution (A,b,(\false C)) ) ; :: thesis: ( ( t1 value_at (C,s) < t2 value_at (C,s) implies f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) < t2 value_at (C,s) ) & ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
A2: f . (s,(b gt (t2,t1,A))) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
reconsider b0 = @ b as Element of G, the bool-sort of S by AOFA_A00:def 22;
A3: (\not (leq (t2,t1))) value_at (C,s) = \not ((leq (t2,t1)) value_at (C,s)) by Th31
.= \not (leq ((t2 value_at (C,s)),(t1 value_at (C,s)))) by Th45 ;
then A4: ((f . (s,(b gt (t2,t1,A)))) . the bool-sort of S) . b = ((succ (s,b0,(\not (leq ((t2 value_at (C,s)),(t1 value_at (C,s))))))) . the bool-sort of S) . b by A1, AOFA_A00:def 28
.= \not (leq ((t2 value_at (C,s)),(t1 value_at (C,s)))) by A1, AOFA_A00:def 27 ;
A5: ( 'not' FALSE = TRUE & TRUE <> FALSE & ( for x being boolean object holds
( x <> FALSE iff x = TRUE ) ) ) by XBOOLEAN:def 3;
\true C = TRUE by AOFA_A00:def 32;
then A6: \false C = 'not' TRUE by AOFA_A00:def 32
.= FALSE ;
( t1 value_at (C,s) < t2 value_at (C,s) iff leq ((t2 value_at (C,s)),(t1 value_at (C,s))) = FALSE ) by AOFA_A00:55;
then ( t1 value_at (C,s) < t2 value_at (C,s) iff \not (leq ((t2 value_at (C,s)),(t1 value_at (C,s)))) <> \false C ) by A6, A3, A5, Th33;
hence ( t1 value_at (C,s) < t2 value_at (C,s) iff f . (s,(b gt (t2,t1,A))) in (\false C) -States ( the generators of G,b) ) by A2, A4, AOFA_A00:def 20; :: thesis: ( ( t1 value_at (C,s) <= t2 value_at (C,s) implies f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) & ( f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) implies t1 value_at (C,s) <= t2 value_at (C,s) ) & ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
A7: f . (s,(b leq (t1,t2,A))) is ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
(leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s))) by Th45;
then A8: ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . b = ((succ (s,b0,(leq ((t1 value_at (C,s)),(t2 value_at (C,s)))))) . the bool-sort of S) . b by A1, AOFA_A00:def 28
.= leq ((t1 value_at (C,s)),(t2 value_at (C,s))) by A1, AOFA_A00:def 27 ;
\true C = TRUE by AOFA_A00:def 32;
then A9: \false C = 'not' TRUE by AOFA_A00:def 32
.= FALSE ;
( t1 value_at (C,s) <= t2 value_at (C,s) iff leq ((t1 value_at (C,s)),(t2 value_at (C,s))) <> \false C ) by A9, AOFA_A00:55;
hence ( t1 value_at (C,s) <= t2 value_at (C,s) iff f . (s,(b leq (t1,t2,A))) in (\false C) -States ( the generators of G,b) ) by A7, A8, AOFA_A00:def 20; :: thesis: ( ( for x being pure Element of the generators of G . I holds
( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x ) ) & ( for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) ) )
b in (FreeGen T) . the bool-sort of S by Def4;
then A10: vf b0 = the bool-sort of S -singleton b by AOFA_A00:41;

hereby :: thesis: for c being pure Element of the generators of G . the bool-sort of S st c <> b holds
( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c )

let x be pure Element of the generators of G . I; :: thesis: ( ((f . (s,(b gt (t1,t2,A)))) . I) . x = (s . I) . x & ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x )
A11: I <> the bool-sort of S by AOFA_A00:53;
A12: x in (FreeGen T) . I by Def4;
A13: x nin (vf b0) . I by A10, A11, AOFA_A00:6;
thus ((f . (s,(b gt (t1,t2,A)))) . I) . x = ((succ (s,b0,((\not (leq (t1,t2))) value_at (C,s)))) . I) . x by A1, AOFA_A00:def 28
.= (s . I) . x by A11, A12, A13, A1, AOFA_A00:def 27 ; :: thesis: ((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . x
thus ((f . (s,(b leq (t1,t2,A)))) . I) . x = ((succ (s,b0,((leq (t1,t2)) value_at (C,s)))) . I) . x by A1, AOFA_A00:def 28
.= (s . I) . x by A11, A12, A13, A1, AOFA_A00:def 27 ; :: thesis: verum

end;

let c be pure Element of the generators of G . the bool-sort of S; :: thesis: ( c <> b implies ( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c ) )
assume A14: c <> b ; :: thesis: ( ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c & ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c )
(vf b0) . the bool-sort of S = {b} by A10, AOFA_A00:6;
then A15: c nin (vf b0) . the bool-sort of S by A14, TARSKI:def 1;
A16: c in (FreeGen T) . the bool-sort of S by Def4;
thus ((f . (s,(b gt (t1,t2,A)))) . the bool-sort of S) . c = ((succ (s,b0,((\not (leq (t1,t2))) value_at (C,s)))) . the bool-sort of S) . c by A1, AOFA_A00:def 28
.= (s . the bool-sort of S) . c by A14, A15, A16, A1, AOFA_A00:def 27 ; :: thesis: ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = (s . the bool-sort of S) . c
thus ((f . (s,(b leq (t1,t2,A)))) . the bool-sort of S) . c = ((succ (s,b0,((leq (t1,t2)) value_at (C,s)))) . the bool-sort of S) . c by A1, AOFA_A00:def 28
.= (s . the bool-sort of S) . c by A14, A15, A16, A1, AOFA_A00:def 27 ; :: thesis: verum