let a be Ordinal; :: thesis: for O being non empty connected Poset
for R being array of O holds {[a,R]} is arr_computation of R
let O be non empty connected Poset; :: thesis: for R being array of O holds {[a,R]} is arr_computation of R
let R be array of O; :: thesis: {[a,R]} is arr_computation of R
reconsider C = {[a,R]} as non empty a -based array ;
C is arr_computation of R
proof
A1: ( dom C = {a} & a in {a} ) by FUNCT_5:12, TARSKI:def 1;
then base- C = a by Def4;
hence C . (base- C) = R by GRFUNC_1:6; :: according to EXCHSORT:def 14 :: thesis: ( ( for a being Ordinal st a in dom C holds
C . a is array of O ) & ( for a being Ordinal st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) )
hereby :: thesis: for a being Ordinal st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) )
let b be Ordinal; :: thesis: ( b in dom C implies C . b is array of O )
assume b in dom C ; :: thesis: C . b is array of O
then a = b by A1, TARSKI:def 1;
hence C . b is array of O by GRFUNC_1:6; :: thesis: verum
end;
let b be Ordinal; :: thesis: ( b in dom C & succ b in dom C implies ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) )
assume ( b in dom C & succ b in dom C ) ; :: thesis: ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) )
then ( a = b & a = succ b ) by A1, TARSKI:def 1;
then a in a by ORDINAL1:6;
hence ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . b = R & C . (succ b) = Swap (R,x,y) ) ; :: thesis: verum
end;
hence {[a,R]} is arr_computation of R ; :: thesis: verum