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 I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
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 I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
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 I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
let I be integer SortSymbol of S; :: thesis: for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
let t1, t2 be Element of T,I; :: thesis: for s being Element of C -States the generators of G holds (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
let s be Element of C -States the generators of G; :: thesis: (t1 mod t2) value_at (C,s) = (t1 value_at (C,s)) mod (t2 value_at (C,s))
thus (t1 mod t2) value_at (C,s) = (t1 - ((t1 div t2) * t2)) value_at (C,s)
.= (t1 value_at (C,s)) - (((t1 div t2) * t2) value_at (C,s)) by Th41
.= (t1 value_at (C,s)) - (((t1 div t2) value_at (C,s)) * (t2 value_at (C,s))) by Th42
.= (t1 value_at (C,s)) mod (t2 value_at (C,s)) by Th43 ; :: thesis: verum