let a be Ordinal; 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; for R being array of O holds {[a,R]} is arr_computation of R
let R be array of O; {[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;
EXCHSORT:def 14 ( ( 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) ) ) )
let b be
Ordinal;
( 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 )
;
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) )
;
verum
end;
hence
{[a,R]} is arr_computation of R
; verum