let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let SCS be non-empty finite-yielding MSAlgebra over IIG; :: thesis: for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let v, w be Vertex of IIG; :: thesis: for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let e1 be Element of the Sorts of (FreeEnv SCS) . v; :: thesis: for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let q1 be DTree-yielding FinSequence; :: thesis: ( v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 implies for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k )
assume that
A1: v in InnerVertices IIG and
A2: e1 = [(action_at v), the carrier of IIG] -tree q1 ; :: thesis: for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
thus for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k :: thesis: verum
proof
reconsider av = action_at v as OperSymbol of IIG ;
let k be Element of NAT ; :: thesis: ( k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w implies w = (the_arity_of (action_at v)) /. k )
assume that
A3: k in dom q1 and
A4: q1 . k in the Sorts of (FreeEnv SCS) . w ; :: thesis: w = (the_arity_of (action_at v)) /. k
A5: FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;
e1 in the Sorts of (FreeEnv SCS) . v ;
then A6: e1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of av) by A1, MSAFREE2:def 7;
then len q1 = len (the_arity_of av) by A2, MSAFREE2:10;
then A7: k in dom (the_arity_of av) by A3, FINSEQ_3:29;
then q1 . k in the Sorts of (FreeEnv SCS) . ((the_arity_of av) . k) by A2, A6, MSAFREE2:11;
then A8: q1 . k in (FreeSort the Sorts of SCS) . ((the_arity_of av) /. k) by A7, A5, PARTFUN1:def 6;
now :: thesis: not (the_arity_of av) /. k <> w
assume (the_arity_of av) /. k <> w ; :: thesis: contradiction
then (FreeSort the Sorts of SCS) . ((the_arity_of av) /. k) misses (FreeSort the Sorts of SCS) . w by MSAFREE:12;
then ((FreeSort the Sorts of SCS) . ((the_arity_of av) /. k)) /\ ((FreeSort the Sorts of SCS) . w) = {} by XBOOLE_0:def 7;
hence contradiction by A4, A5, A8, XBOOLE_0:def 4; :: thesis: verum
end;
hence w = (the_arity_of (action_at v)) /. k ; :: thesis: verum
end;