let S be non empty non void bool-correct 4,1 integer BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being b1,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 V3() ManySortedSet of the carrier of S; 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; 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; 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; 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; 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; 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; 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; 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; 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); ( 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)) )
; ( ( 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; ( ( 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; ( ( 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 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;
( ((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
;
((f . (s,(b leq (t1,t2,A)))) . I) . x = (s . I) . xthus ((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
;
verum
end;
let c be pure Element of the generators of G . the bool-sort of S; ( 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
; ( ((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
; ((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
; verum