:: AMI_4 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
K6(NAT) is set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
K126(9) is Element of K6(NAT)
K191() is set
K198() is set
K6(K198()) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
K7(K198(),2) is Relation-like set
K6(K7(K198(),2)) is set
K200() is Relation-like K198() -defined 2 -valued Function-like V40(K198(),2) Element of K6(K7(K198(),2))
K201() is Relation-like 2 -defined Function-like total set
K200() * K201() is Relation-like K198() -defined set
K180((K200() * K201())) is set
K192() is non empty set
K152(K180((K200() * K201())),K180((K200() * K201()))) is set
K7(K192(),K152(K180((K200() * K201())),K180((K200() * K201())))) is Relation-like set
K6(K7(K192(),K152(K180((K200() * K201())),K180((K200() * K201()))))) is set
SCM is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the InstructionsF of SCM is non empty Relation-like V72() V73() V74() V76() set
the carrier of SCM is non empty set
K286(2,SCM) is Relation-like non-empty the carrier of SCM -defined Function-like total set
the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like V40( the carrier of SCM,2) Element of K6(K7( the carrier of SCM,2))
K7( the carrier of SCM,2) is Relation-like set
K6(K7( the carrier of SCM,2)) is set
the U7 of SCM is Relation-like 2 -defined Function-like total set
the Object-Kind of SCM * the U7 of SCM is Relation-like the carrier of SCM -defined set
RAT is set
INT is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
IC is V51( SCM ) Element of the carrier of SCM
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
{{},1,2,3,4} is finite set
dl. 0 is V63() Element of the carrier of SCM
dl. 1 is V63() Element of the carrier of SCM
dl. 2 is V63() Element of the carrier of SCM
(dl. 2) := (dl. 1) is Element of the InstructionsF of SCM
0 .--> ((dl. 2) := (dl. 1)) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{0} is non empty finite V32() set
{0} --> ((dl. 2) := (dl. 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM -valued {((dl. 2) := (dl. 1))} -valued Function-like constant finite total V40({0},{((dl. 2) := (dl. 1))}) Element of K6(K7({0},{((dl. 2) := (dl. 1))}))
{((dl. 2) := (dl. 1))} is non empty finite set
K7({0},{((dl. 2) := (dl. 1))}) is Relation-like finite set
K6(K7({0},{((dl. 2) := (dl. 1))})) is finite V32() set
Divide ((dl. 0),(dl. 1)) is Element of the InstructionsF of SCM
1 .--> (Divide ((dl. 0),(dl. 1))) is V2() Relation-like NAT -defined {1} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{1} is non empty finite V64() V65() set
{1} --> (Divide ((dl. 0),(dl. 1))) is non empty Relation-like {1} -defined the InstructionsF of SCM -valued {(Divide ((dl. 0),(dl. 1)))} -valued Function-like constant finite total V40({1},{(Divide ((dl. 0),(dl. 1)))}) Element of K6(K7({1},{(Divide ((dl. 0),(dl. 1)))}))
{(Divide ((dl. 0),(dl. 1)))} is non empty finite set
K7({1},{(Divide ((dl. 0),(dl. 1)))}) is Relation-like finite set
K6(K7({1},{(Divide ((dl. 0),(dl. 1)))})) is finite V32() set
(dl. 0) := (dl. 2) is Element of the InstructionsF of SCM
2 .--> ((dl. 0) := (dl. 2)) is V2() Relation-like NAT -defined {2} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{2} is non empty finite V64() V65() set
{2} --> ((dl. 0) := (dl. 2)) is non empty Relation-like {2} -defined the InstructionsF of SCM -valued {((dl. 0) := (dl. 2))} -valued Function-like constant finite total V40({2},{((dl. 0) := (dl. 2))}) Element of K6(K7({2},{((dl. 0) := (dl. 2))}))
{((dl. 0) := (dl. 2))} is non empty finite set
K7({2},{((dl. 0) := (dl. 2))}) is Relation-like finite set
K6(K7({2},{((dl. 0) := (dl. 2))})) is finite V32() set
(dl. 1) >0_goto 0 is Element of the InstructionsF of SCM
3 .--> ((dl. 1) >0_goto 0) is V2() Relation-like NAT -defined {3} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{3} is non empty finite V64() V65() set
{3} --> ((dl. 1) >0_goto 0) is non empty Relation-like {3} -defined the InstructionsF of SCM -valued {((dl. 1) >0_goto 0)} -valued Function-like constant finite total V40({3},{((dl. 1) >0_goto 0)}) Element of K6(K7({3},{((dl. 1) >0_goto 0)}))
{((dl. 1) >0_goto 0)} is non empty finite set
K7({3},{((dl. 1) >0_goto 0)}) is Relation-like finite set
K6(K7({3},{((dl. 1) >0_goto 0)})) is finite V32() set
halt SCM is Element of the InstructionsF of SCM
K273( the InstructionsF of SCM) is V75( the InstructionsF of SCM) Element of the InstructionsF of SCM
4 .--> (halt SCM) is V2() Relation-like NAT -defined {4} -defined the InstructionsF of SCM -valued Function-like one-to-one finite set
{4} is non empty finite V64() V65() set
{4} --> (halt SCM) is non empty Relation-like {4} -defined the InstructionsF of SCM -valued {(halt SCM)} -valued Function-like constant finite total V40({4},{(halt SCM)}) Element of K6(K7({4},{(halt SCM)}))
{(halt SCM)} is non empty finite set
K7({4},{(halt SCM)}) is Relation-like finite set
K6(K7({4},{(halt SCM)})) is finite V32() set
(3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
(0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
() is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like finite set
dom () is finite set
dom (3 .--> ((dl. 1) >0_goto 0)) is V2() finite set
dom (4 .--> (halt SCM)) is V2() finite set
dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is finite set
{3} \/ {4} is non empty finite V64() V65() set
{3,4} is non empty finite V64() V65() set
dom (1 .--> (Divide ((dl. 0),(dl. 1)))) is V2() finite set
dom (2 .--> ((dl. 0) := (dl. 2))) is V2() finite set
dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is finite set
{2} \/ {3,4} is non empty finite V64() V65() set
{2,3,4} is finite V64() set
dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is finite set
{1} \/ {2,3,4} is non empty finite V64() V65() set
{1,2,3,4} is finite V64() set
dom (0 .--> ((dl. 2) := (dl. 1))) is V2() finite set
dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) is finite set
{0} \/ {1,2,3,4} is non empty finite set
q is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
q . 0 is Element of the InstructionsF of SCM
q . 1 is Element of the InstructionsF of SCM
q . 2 is Element of the InstructionsF of SCM
q . 3 is Element of the InstructionsF of SCM
dom (4 .--> (halt SCM)) is V2() finite set
dom (3 .--> ((dl. 1) >0_goto 0)) is V2() finite set
dom ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is finite set
{3} \/ {4} is non empty finite V64() V65() set
{3,4} is non empty finite V64() V65() set
dom (2 .--> ((dl. 0) := (dl. 2))) is V2() finite set
dom ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is finite set
{2} \/ {3,4} is non empty finite V64() V65() set
{2,3,4} is finite V64() set
dom (1 .--> (Divide ((dl. 0),(dl. 1)))) is V2() finite set
dom ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is finite set
{1} \/ {2,3,4} is non empty finite V64() V65() set
{1,2,3,4} is finite V64() set
dom ((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) is finite set
((0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))))) . 0 is set
(0 .--> ((dl. 2) := (dl. 1))) . 0 is set
((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) . 1 is set
(1 .--> (Divide ((dl. 0),(dl. 1)))) . 1 is set
((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) . 2 is set
(2 .--> ((dl. 0) := (dl. 2))) . 2 is set
((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) . 3 is set
(3 .--> ((dl. 1) >0_goto 0)) . 3 is set
q . 4 is Element of the InstructionsF of SCM
((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) . 4 is set
(4 .--> (halt SCM)) . 4 is set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 2) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec (((dl. 2) := (dl. 1)),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 2) := (dl. 1))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 2) := (dl. 1))) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
((Comput (p,q,x)) . (dl. 0)) div ((Comput (p,q,x)) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (p,q,x)) . (dl. 0)) mod ((Comput (p,q,x)) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 2) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec ((Divide ((dl. 0),(dl. 1))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(Divide ((dl. 0),(dl. 1)))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(Divide ((dl. 0),(dl. 1)))) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 2) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 2) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec (((dl. 0) := (dl. 2)),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 0) := (dl. 2))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 0) := (dl. 2))) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
(Comput (p,q,x)) . (dl. 1) is V11() V12() integer ext-real set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(x + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(x + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(x + 1))) . (IC ) is set
(Comput (p,q,(x + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,x)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,(x + 1))) . (dl. 1) is V11() V12() integer ext-real set
p . (IC (Comput (p,q,x))) is Element of the InstructionsF of SCM
Exec ((p . (IC (Comput (p,q,x)))),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K180(( the Object-Kind of SCM * the U7 of SCM)) is set
K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) is set
the Execution of SCM is Relation-like the InstructionsF of SCM -defined K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))) -valued Function-like V40( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) Element of K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))))
K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))) is Relation-like set
K6(K7( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))))) is set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,(p . (IC (Comput (p,q,x))))) . (Comput (p,q,x)) is set
Exec (((dl. 1) >0_goto 0),(Comput (p,q,x))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 1) >0_goto 0)) is Element of K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM)))
K154( the InstructionsF of SCM,K152(K180(( the Object-Kind of SCM * the U7 of SCM)),K180(( the Object-Kind of SCM * the U7 of SCM))), the Execution of SCM,((dl. 1) >0_goto 0)) . (Comput (p,q,x)) is set
succ (IC (Comput (p,q,x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,x)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,x)) . (IC ) is set
i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
x + i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(x + i1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
p is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
p . (dl. 0) is V11() V12() integer ext-real set
p . (dl. 1) is V11() V12() integer ext-real set
x is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (x,p,(4 * q)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * q))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * q))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * q))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * q))) . (IC ) is set
IC p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
p . (IC ) is set
i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (x,p,(4 * i1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * i1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * i1))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * i1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * i1))) . (IC ) is set
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (i1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (x,p,(4 * (i1 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * (i1 + 1)))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * (i1 + 1)))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * (i1 + 1)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * (i1 + 1)))) . (IC ) is set
(4 * i1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * i1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * i1) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 3)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * i1) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * i1) + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * i1) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * i1) + 2) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * i1) + 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * i1) + 3) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * i1) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * i1) + 1) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * i1) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 1))) . (IC ) is set
IC (Comput (x,p,((4 * i1) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 2))) . (IC ) is set
IC (Comput (x,p,((4 * i1) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 3))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 2))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 1))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (x,p,((4 * i1) + 1))) . (dl. 0)) mod ((Comput (x,p,((4 * i1) + 1))) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 1))) . (dl. 2) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
(Comput (x,p,((4 * i1) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * i1) + 4))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,((4 * i1) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * i1) + 4))) . (IC ) is set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (x,p,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * 0))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * 0))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (x,p,(4 * 0))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * 0))) . (IC ) is set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (q + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
p is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
p . (dl. 0) is V11() V12() integer ext-real set
p . (dl. 1) is V11() V12() integer ext-real set
x is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (x,p,(4 * q)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * q))) . (dl. 1) is V11() V12() integer ext-real set
Comput (x,p,(4 * (q + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (x,p,(4 * (q + 1)))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,(4 * (q + 1)))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,(4 * q))) . (dl. 0) is V11() V12() integer ext-real set
((Comput (x,p,(4 * q))) . (dl. 0)) mod ((Comput (x,p,(4 * q))) . (dl. 1)) is V11() V12() integer ext-real set
(4 * q) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * q) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(4 * q) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 3)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,(4 * q))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,(4 * q))) . (IC ) is set
((4 * q) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * q) + 1) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * q) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * q) + 1))) . (IC ) is set
(Comput (x,p,((4 * q) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 1))) . (dl. 2) is V11() V12() integer ext-real set
((4 * q) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * q) + 2) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * q) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * q) + 2))) . (IC ) is set
(4 * q) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,((4 * q) + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
((4 * q) + 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (x,p,(((4 * q) + 3) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (x,p,((4 * q) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (x,p,((4 * q) + 3))) . (IC ) is set
(Comput (x,p,((4 * q) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 2))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (x,p,((4 * q) + 1))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (x,p,((4 * q) + 1))) . (dl. 0)) mod ((Comput (x,p,((4 * q) + 1))) . (dl. 1)) is V11() V12() integer ext-real set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
q . (dl. 0) is V11() V12() integer ext-real set
q . (dl. 1) is V11() V12() integer ext-real set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Result (p,q) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (p,q)) . (dl. 0) is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
i1 is V11() V12() integer ext-real set
x gcd i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * i2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * i2))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * i2))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (i2 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * (i2 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * (i2 + 1)))) . (dl. 0) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * (i2 + 1)))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * i2))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (p,q,(4 * (i2 + 1)))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * (i2 + 1)))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((Comput (p,q,(4 * i2))) . (dl. 0)) mod ((Comput (p,q,(4 * i2))) . (dl. 1)) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * i2))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
H₂(i2) mod H₁(i2) is V11() V12() integer ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (p,q,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * 0))) . (dl. 0) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * 0))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
abs x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * 0))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * 0))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
abs i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
4 * t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * t)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (p,q,(4 * t))) . (dl. 0) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * t))) . (dl. 0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * t))) . (dl. 1) is V11() V12() integer ext-real set
abs ((Comput (p,q,(4 * t))) . (dl. 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
IC (Comput (p,q,(4 * t))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(4 * t))) . (IC ) is set
q is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total 0 -started set
q . (dl. 0) is V11() V12() integer ext-real set
q . (dl. 1) is V11() V12() integer ext-real set
p is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Result (p,q) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (p,q)) . (dl. 0) is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
i1 is V11() V12() integer ext-real set
x gcd i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
abs i1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,4) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (p,q,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * (0 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
x mod i1 is V11() V12() integer ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 mod d is V11() V12() integer ext-real set
t . (dl. 1) is V11() V12() integer ext-real set
IC t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
t . (IC ) is set
t . (dl. 0) is V11() V12() integer ext-real set
Comput (p,q,4) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,q,(4 * (0 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (p,q,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t . (dl. 0) is V11() V12() integer ext-real set
x mod i1 is V11() V12() integer ext-real set
i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i2 mod d is V11() V12() integer ext-real set
t . (dl. 1) is V11() V12() integer ext-real set
IC t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
t . (IC ) is set
T is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (p,t,T) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,t,T)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,t,T)) . (IC ) is set
T + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (p,q,(T + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (p,q,(T + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (p,q,(T + 4))) . (IC ) is set
Result (p,t) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (p,t)) . (dl. 0) is V11() V12() integer ext-real set
FinPartSt SCM is non empty Element of K6(K184(K286(2,SCM)))
K184(K286(2,SCM)) is set
K6(K184(K286(2,SCM))) is set
{ b₁ where b₁ is Element of K184(K286(2,SCM)) : b₁ is finite } is set
K7((FinPartSt SCM),(FinPartSt SCM)) is Relation-like set
K6(K7((FinPartSt SCM),(FinPartSt SCM))) is set
q is set
p is set
x is set
i1 is V11() V12() integer ext-real set
i2 is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i1,i2) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i1 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i1 is non empty Relation-like {(dl. 0)} -defined {i1} -valued Function-like constant finite total V40({(dl. 0)},{i1}) Element of K6(K7({(dl. 0)},{i1}))
{i1} is non empty finite set
K7({(dl. 0)},{i1}) is Relation-like finite set
K6(K7({(dl. 0)},{i1})) is finite V32() set
(dl. 1) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> i2 is non empty Relation-like {(dl. 1)} -defined {i2} -valued Function-like constant finite total V40({(dl. 1)},{i2}) Element of K6(K7({(dl. 1)},{i2}))
{i2} is non empty finite set
K7({(dl. 1)},{i2}) is Relation-like finite set
K6(K7({(dl. 1)},{i2})) is finite V32() set
((dl. 0) .--> i1) +* ((dl. 1) .--> i2) is Relation-like the carrier of SCM -defined Function-like finite set
i1 gcd i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i1 gcd i2) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i1 gcd i2) is non empty Relation-like {(dl. 0)} -defined {(i1 gcd i2)} -valued Function-like constant finite total V40({(dl. 0)},{(i1 gcd i2)}) Element of K6(K7({(dl. 0)},{(i1 gcd i2)}))
{(i1 gcd i2)} is non empty finite set
K7({(dl. 0)},{(i1 gcd i2)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i1 gcd i2)})) is finite V32() set
d is V11() V12() integer ext-real set
t is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (d,t) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> d is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} --> d is non empty Relation-like {(dl. 0)} -defined {d} -valued Function-like constant finite total V40({(dl. 0)},{d}) Element of K6(K7({(dl. 0)},{d}))
{d} is non empty finite set
K7({(dl. 0)},{d}) is Relation-like finite set
K6(K7({(dl. 0)},{d})) is finite V32() set
(dl. 1) .--> t is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} --> t is non empty Relation-like {(dl. 1)} -defined {t} -valued Function-like constant finite total V40({(dl. 1)},{t}) Element of K6(K7({(dl. 1)},{t}))
{t} is non empty finite set
K7({(dl. 1)},{t}) is Relation-like finite set
K6(K7({(dl. 1)},{t})) is finite V32() set
((dl. 0) .--> d) +* ((dl. 1) .--> t) is Relation-like the carrier of SCM -defined Function-like finite set
d gcd t is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (d gcd t) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (d gcd t) is non empty Relation-like {(dl. 0)} -defined {(d gcd t)} -valued Function-like constant finite total V40({(dl. 0)},{(d gcd t)}) Element of K6(K7({(dl. 0)},{(d gcd t)}))
{(d gcd t)} is non empty finite set
K7({(dl. 0)},{(d gcd t)}) is Relation-like finite set
K6(K7({(dl. 0)},{(d gcd t)})) is finite V32() set
(((dl. 0),(dl. 1)) --> (i1,i2)) . (dl. 1) is set
(((dl. 0),(dl. 1)) --> (i1,i2)) . (dl. 0) is set
q is Relation-like Function-like set
rng q is set
p is set
x is set
[x,p] is set
{x,p} is non empty finite set
{x} is non empty finite set
{{x,p},{x}} is non empty finite V32() V64() V65() set
i1 is V11() V12() integer ext-real set
i2 is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i1,i2) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i1 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i1 is non empty Relation-like {(dl. 0)} -defined {i1} -valued Function-like constant finite total V40({(dl. 0)},{i1}) Element of K6(K7({(dl. 0)},{i1}))
{i1} is non empty finite set
K7({(dl. 0)},{i1}) is Relation-like finite set
K6(K7({(dl. 0)},{i1})) is finite V32() set
(dl. 1) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> i2 is non empty Relation-like {(dl. 1)} -defined {i2} -valued Function-like constant finite total V40({(dl. 1)},{i2}) Element of K6(K7({(dl. 1)},{i2}))
{i2} is non empty finite set
K7({(dl. 1)},{i2}) is Relation-like finite set
K6(K7({(dl. 1)},{i2})) is finite V32() set
((dl. 0) .--> i1) +* ((dl. 1) .--> i2) is Relation-like the carrier of SCM -defined Function-like finite set
i1 gcd i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i1 gcd i2) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i1 gcd i2) is non empty Relation-like {(dl. 0)} -defined {(i1 gcd i2)} -valued Function-like constant finite total V40({(dl. 0)},{(i1 gcd i2)}) Element of K6(K7({(dl. 0)},{(i1 gcd i2)}))
{(i1 gcd i2)} is non empty finite set
K7({(dl. 0)},{(i1 gcd i2)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i1 gcd i2)})) is finite V32() set
dom q is set
p is set
q . p is set
[p,(q . p)] is set
{p,(q . p)} is non empty finite set
{p} is non empty finite set
{{p,(q . p)},{p}} is non empty finite V32() V64() V65() set
p is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
x is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
i1 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
[x,i1] is set
{x,i1} is non empty finite V32() set
{x} is non empty finite V32() set
{{x,i1},{x}} is non empty finite V32() V64() V65() set
i2 is V11() V12() integer ext-real set
d is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i2,d) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i2 is non empty Relation-like {(dl. 0)} -defined {i2} -valued Function-like constant finite total V40({(dl. 0)},{i2}) Element of K6(K7({(dl. 0)},{i2}))
{i2} is non empty finite set
K7({(dl. 0)},{i2}) is Relation-like finite set
K6(K7({(dl. 0)},{i2})) is finite V32() set
(dl. 1) .--> d is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> d is non empty Relation-like {(dl. 1)} -defined {d} -valued Function-like constant finite total V40({(dl. 1)},{d}) Element of K6(K7({(dl. 1)},{d}))
{d} is non empty finite set
K7({(dl. 1)},{d}) is Relation-like finite set
K6(K7({(dl. 1)},{d})) is finite V32() set
((dl. 0) .--> i2) +* ((dl. 1) .--> d) is Relation-like the carrier of SCM -defined Function-like finite set
i2 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i2 gcd d) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i2 gcd d) is non empty Relation-like {(dl. 0)} -defined {(i2 gcd d)} -valued Function-like constant finite total V40({(dl. 0)},{(i2 gcd d)}) Element of K6(K7({(dl. 0)},{(i2 gcd d)}))
{(i2 gcd d)} is non empty finite set
K7({(dl. 0)},{(i2 gcd d)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i2 gcd d)})) is finite V32() set
q is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
p is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
x is Element of FinPartSt SCM
i1 is Element of FinPartSt SCM
[x,i1] is set
{x,i1} is non empty finite set
{x} is non empty finite set
{{x,i1},{x}} is non empty finite V32() V64() V65() set
i2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
d is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
t is V11() V12() integer ext-real set
T is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (t,T) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> t is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> t is non empty Relation-like {(dl. 0)} -defined {t} -valued Function-like constant finite total V40({(dl. 0)},{t}) Element of K6(K7({(dl. 0)},{t}))
{t} is non empty finite set
K7({(dl. 0)},{t}) is Relation-like finite set
K6(K7({(dl. 0)},{t})) is finite V32() set
(dl. 1) .--> T is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> T is non empty Relation-like {(dl. 1)} -defined {T} -valued Function-like constant finite total V40({(dl. 1)},{T}) Element of K6(K7({(dl. 1)},{T}))
{T} is non empty finite set
K7({(dl. 1)},{T}) is Relation-like finite set
K6(K7({(dl. 1)},{T})) is finite V32() set
((dl. 0) .--> t) +* ((dl. 1) .--> T) is Relation-like the carrier of SCM -defined Function-like finite set
t gcd T is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (t gcd T) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (t gcd T) is non empty Relation-like {(dl. 0)} -defined {(t gcd T)} -valued Function-like constant finite total V40({(dl. 0)},{(t gcd T)}) Element of K6(K7({(dl. 0)},{(t gcd T)}))
{(t gcd T)} is non empty finite set
K7({(dl. 0)},{(t gcd T)}) is Relation-like finite set
K6(K7({(dl. 0)},{(t gcd T)})) is finite V32() set
i2 is V11() V12() integer ext-real set
d is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i2,d) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i2 is non empty Relation-like {(dl. 0)} -defined {i2} -valued Function-like constant finite total V40({(dl. 0)},{i2}) Element of K6(K7({(dl. 0)},{i2}))
{i2} is non empty finite set
K7({(dl. 0)},{i2}) is Relation-like finite set
K6(K7({(dl. 0)},{i2})) is finite V32() set
(dl. 1) .--> d is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> d is non empty Relation-like {(dl. 1)} -defined {d} -valued Function-like constant finite total V40({(dl. 1)},{d}) Element of K6(K7({(dl. 1)},{d}))
{d} is non empty finite set
K7({(dl. 1)},{d}) is Relation-like finite set
K6(K7({(dl. 1)},{d})) is finite V32() set
((dl. 0) .--> i2) +* ((dl. 1) .--> d) is Relation-like the carrier of SCM -defined Function-like finite set
i2 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i2 gcd d) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i2 gcd d) is non empty Relation-like {(dl. 0)} -defined {(i2 gcd d)} -valued Function-like constant finite total V40({(dl. 0)},{(i2 gcd d)}) Element of K6(K7({(dl. 0)},{(i2 gcd d)}))
{(i2 gcd d)} is non empty finite set
K7({(dl. 0)},{(i2 gcd d)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i2 gcd d)})) is finite V32() set
x is Element of FinPartSt SCM
i1 is Element of FinPartSt SCM
[x,i1] is set
{x,i1} is non empty finite set
{x} is non empty finite set
{{x,i1},{x}} is non empty finite V32() V64() V65() set
i2 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
d is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
t is V11() V12() integer ext-real set
T is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (t,T) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> t is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> t is non empty Relation-like {(dl. 0)} -defined {t} -valued Function-like constant finite total V40({(dl. 0)},{t}) Element of K6(K7({(dl. 0)},{t}))
{t} is non empty finite set
K7({(dl. 0)},{t}) is Relation-like finite set
K6(K7({(dl. 0)},{t})) is finite V32() set
(dl. 1) .--> T is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> T is non empty Relation-like {(dl. 1)} -defined {T} -valued Function-like constant finite total V40({(dl. 1)},{T}) Element of K6(K7({(dl. 1)},{T}))
{T} is non empty finite set
K7({(dl. 1)},{T}) is Relation-like finite set
K6(K7({(dl. 1)},{T})) is finite V32() set
((dl. 0) .--> t) +* ((dl. 1) .--> T) is Relation-like the carrier of SCM -defined Function-like finite set
t gcd T is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (t gcd T) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (t gcd T) is non empty Relation-like {(dl. 0)} -defined {(t gcd T)} -valued Function-like constant finite total V40({(dl. 0)},{(t gcd T)}) Element of K6(K7({(dl. 0)},{(t gcd T)}))
{(t gcd T)} is non empty finite set
K7({(dl. 0)},{(t gcd T)}) is Relation-like finite set
K6(K7({(dl. 0)},{(t gcd T)})) is finite V32() set
i2 is V11() V12() integer ext-real set
d is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i2,d) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i2 is non empty Relation-like {(dl. 0)} -defined {i2} -valued Function-like constant finite total V40({(dl. 0)},{i2}) Element of K6(K7({(dl. 0)},{i2}))
{i2} is non empty finite set
K7({(dl. 0)},{i2}) is Relation-like finite set
K6(K7({(dl. 0)},{i2})) is finite V32() set
(dl. 1) .--> d is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> d is non empty Relation-like {(dl. 1)} -defined {d} -valued Function-like constant finite total V40({(dl. 1)},{d}) Element of K6(K7({(dl. 1)},{d}))
{d} is non empty finite set
K7({(dl. 1)},{d}) is Relation-like finite set
K6(K7({(dl. 1)},{d})) is finite V32() set
((dl. 0) .--> i2) +* ((dl. 1) .--> d) is Relation-like the carrier of SCM -defined Function-like finite set
i2 gcd d is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i2 gcd d) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i2 gcd d) is non empty Relation-like {(dl. 0)} -defined {(i2 gcd d)} -valued Function-like constant finite total V40({(dl. 0)},{(i2 gcd d)}) Element of K6(K7({(dl. 0)},{(i2 gcd d)}))
{(i2 gcd d)} is non empty finite set
K7({(dl. 0)},{(i2 gcd d)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i2 gcd d)})) is finite V32() set
() is Relation-like FinPartSt SCM -defined FinPartSt SCM -valued Function-like Element of K6(K7((FinPartSt SCM),(FinPartSt SCM)))
dom () is set
q is set
() . q is set
[q,(() . q)] is set
{q,(() . q)} is non empty finite set
{q} is non empty finite set
{{q,(() . q)},{q}} is non empty finite V32() V64() V65() set
p is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (p,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> p is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> p is non empty Relation-like {(dl. 0)} -defined {p} -valued Function-like constant finite total V40({(dl. 0)},{p}) Element of K6(K7({(dl. 0)},{p}))
{p} is non empty finite set
K7({(dl. 0)},{p}) is Relation-like finite set
K6(K7({(dl. 0)},{p})) is finite V32() set
(dl. 1) .--> x is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> x is non empty Relation-like {(dl. 1)} -defined {x} -valued Function-like constant finite total V40({(dl. 1)},{x}) Element of K6(K7({(dl. 1)},{x}))
{x} is non empty finite set
K7({(dl. 1)},{x}) is Relation-like finite set
K6(K7({(dl. 1)},{x})) is finite V32() set
((dl. 0) .--> p) +* ((dl. 1) .--> x) is Relation-like the carrier of SCM -defined Function-like finite set
p gcd x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (p gcd x) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (p gcd x) is non empty Relation-like {(dl. 0)} -defined {(p gcd x)} -valued Function-like constant finite total V40({(dl. 0)},{(p gcd x)}) Element of K6(K7({(dl. 0)},{(p gcd x)}))
{(p gcd x)} is non empty finite set
K7({(dl. 0)},{(p gcd x)}) is Relation-like finite set
K6(K7({(dl. 0)},{(p gcd x)})) is finite V32() set
p is V11() V12() integer ext-real set
x is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (p,x) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> p is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> p is non empty Relation-like {(dl. 0)} -defined {p} -valued Function-like constant finite total V40({(dl. 0)},{p}) Element of K6(K7({(dl. 0)},{p}))
{p} is non empty finite set
K7({(dl. 0)},{p}) is Relation-like finite set
K6(K7({(dl. 0)},{p})) is finite V32() set
(dl. 1) .--> x is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> x is non empty Relation-like {(dl. 1)} -defined {x} -valued Function-like constant finite total V40({(dl. 1)},{x}) Element of K6(K7({(dl. 1)},{x}))
{x} is non empty finite set
K7({(dl. 1)},{x}) is Relation-like finite set
K6(K7({(dl. 1)},{x})) is finite V32() set
((dl. 0) .--> p) +* ((dl. 1) .--> x) is Relation-like the carrier of SCM -defined Function-like finite set
p gcd x is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (p gcd x) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (p gcd x) is non empty Relation-like {(dl. 0)} -defined {(p gcd x)} -valued Function-like constant finite total V40({(dl. 0)},{(p gcd x)}) Element of K6(K7({(dl. 0)},{(p gcd x)}))
{(p gcd x)} is non empty finite set
K7({(dl. 0)},{(p gcd x)}) is Relation-like finite set
K6(K7({(dl. 0)},{(p gcd x)})) is finite V32() set
[q,((dl. 0) .--> (p gcd x))] is set
{q,((dl. 0) .--> (p gcd x))} is non empty finite set
{{q,((dl. 0) .--> (p gcd x))},{q}} is non empty finite V32() V64() V65() set
q is V11() V12() integer ext-real set
p is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (q,p) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> q is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> q is non empty Relation-like {(dl. 0)} -defined {q} -valued Function-like constant finite total V40({(dl. 0)},{q}) Element of K6(K7({(dl. 0)},{q}))
{q} is non empty finite set
K7({(dl. 0)},{q}) is Relation-like finite set
K6(K7({(dl. 0)},{q})) is finite V32() set
(dl. 1) .--> p is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> p is non empty Relation-like {(dl. 1)} -defined {p} -valued Function-like constant finite total V40({(dl. 1)},{p}) Element of K6(K7({(dl. 1)},{p}))
{p} is non empty finite set
K7({(dl. 1)},{p}) is Relation-like finite set
K6(K7({(dl. 1)},{p})) is finite V32() set
((dl. 0) .--> q) +* ((dl. 1) .--> p) is Relation-like the carrier of SCM -defined Function-like finite set
() . (((dl. 0),(dl. 1)) --> (q,p)) is set
q gcd p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (q gcd p) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (q gcd p) is non empty Relation-like {(dl. 0)} -defined {(q gcd p)} -valued Function-like constant finite total V40({(dl. 0)},{(q gcd p)}) Element of K6(K7({(dl. 0)},{(q gcd p)}))
{(q gcd p)} is non empty finite set
K7({(dl. 0)},{(q gcd p)}) is Relation-like finite set
K6(K7({(dl. 0)},{(q gcd p)})) is finite V32() set
[(((dl. 0),(dl. 1)) --> (q,p)),((dl. 0) .--> (q gcd p))] is set
{(((dl. 0),(dl. 1)) --> (q,p)),((dl. 0) .--> (q gcd p))} is non empty finite V32() set
{(((dl. 0),(dl. 1)) --> (q,p))} is non empty finite V32() set
{{(((dl. 0),(dl. 1)) --> (q,p)),((dl. 0) .--> (q gcd p))},{(((dl. 0),(dl. 1)) --> (q,p))}} is non empty finite V32() V64() V65() set
rng (4 .--> (halt SCM)) is V2() finite set
rng ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))) is finite set
rng ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM)))) is finite set
rng ((1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> (halt SCM))))) is finite set
rng () is finite set
Start-At (0,SCM) is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite 0 -started set
(IC ) .--> 0 is V2() Relation-like the carrier of SCM -defined {(IC )} -defined NAT -valued Function-like one-to-one finite set
{(IC )} is non empty finite set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued {0} -valued Function-like constant finite total V40({(IC )},{0}) Element of K6(K7({(IC )},{0}))
K7({(IC )},{0}) is Relation-like finite set
K6(K7({(IC )},{0})) is finite V32() set
x is set
DataPart (Start-At (0,SCM)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite data-only set
NonZero SCM is Element of K6( the carrier of SCM)
K6( the carrier of SCM) is set
(Start-At (0,SCM)) | (NonZero SCM) is Relation-like NonZero SCM -defined the carrier of SCM -defined finite set
dom (DataPart (Start-At (0,SCM))) is finite set
i1 is V11() V12() integer ext-real set
i2 is V11() V12() integer ext-real set
((dl. 0),(dl. 1)) --> (i1,i2) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(dl. 0) .--> i1 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one finite set
{(dl. 0)} is non empty finite set
{(dl. 0)} --> i1 is non empty Relation-like {(dl. 0)} -defined {i1} -valued Function-like constant finite total V40({(dl. 0)},{i1}) Element of K6(K7({(dl. 0)},{i1}))
{i1} is non empty finite set
K7({(dl. 0)},{i1}) is Relation-like finite set
K6(K7({(dl. 0)},{i1})) is finite V32() set
(dl. 1) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one finite set
{(dl. 1)} is non empty finite set
{(dl. 1)} --> i2 is non empty Relation-like {(dl. 1)} -defined {i2} -valued Function-like constant finite total V40({(dl. 1)},{i2}) Element of K6(K7({(dl. 1)},{i2}))
{i2} is non empty finite set
K7({(dl. 1)},{i2}) is Relation-like finite set
K6(K7({(dl. 1)},{i2})) is finite V32() set
((dl. 0) .--> i1) +* ((dl. 1) .--> i2) is Relation-like the carrier of SCM -defined Function-like finite set
(dl. 0) .--> i1 is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
(dl. 1) .--> i2 is V2() Relation-like the carrier of SCM -defined {(dl. 1)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
((dl. 0) .--> i1) +* ((dl. 1) .--> i2) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
d is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
(Start-At (0,SCM)) +* d is non empty Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
t is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
T is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
dom d is finite set
{(dl. 0),(dl. 1)} is non empty finite set
A is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
A . (dl. 0) is V11() V12() integer ext-real set
A . (dl. 1) is V11() V12() integer ext-real set
d . (dl. 0) is set
d . (dl. 1) is set
dom (Start-At (0,SCM)) is non empty finite set
A is set
(dom (Start-At (0,SCM))) /\ (dom d) is finite set
{(IC ),(dl. 0),(dl. 1)} is finite set
dom ((Start-At (0,SCM)) +* d) is non empty finite set
(dom (Start-At (0,SCM))) \/ (dom d) is non empty finite set
{(IC )} \/ (dom (DataPart (Start-At (0,SCM)))) is non empty finite set
({(IC )} \/ (dom (DataPart (Start-At (0,SCM))))) \/ (dom d) is non empty finite set
{(IC )} \/ {(dl. 0),(dl. 1)} is non empty finite set
IC ((Start-At (0,SCM)) +* d) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((Start-At (0,SCM)) +* d) . (IC ) is set
IC (Start-At (0,SCM)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Start-At (0,SCM)) . (IC ) is set
t is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
P is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
t9 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
k0 is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
k0 . (dl. 0) is V11() V12() integer ext-real set
k0 . (dl. 1) is V11() V12() integer ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (t,t9,k) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (t,t9,k)) | (dom ((Start-At (0,SCM)) +* d)) is Relation-like dom ((Start-At (0,SCM)) +* d) -defined the carrier of SCM -defined finite set
Comput (P,k0,k) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P,k0,k)) | (dom ((Start-At (0,SCM)) +* d)) is Relation-like dom ((Start-At (0,SCM)) +* d) -defined the carrier of SCM -defined finite set
Comput (t,t9,0) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
Comput (P,k0,0) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
dom (Comput (t,t9,k)) is set
dom (Comput (P,k0,k)) is set
i is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
4 * i is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (t,t9,(4 * i)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (t,t9,(4 * i))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,(4 * i))) . (IC ) is set
Comput (P,k0,(4 * i)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,k0,(4 * i))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,(4 * i))) . (IC ) is set
(Comput (t,t9,(4 * i))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (P,k0,(4 * i))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,(4 * i))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,(4 * i))) . (dl. 1) is V11() V12() integer ext-real set
j is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(4 * i) + j is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (t,t9,((4 * i) + j)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (t,t9,((4 * i) + j))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,((4 * i) + j))) . (IC ) is set
Comput (P,k0,((4 * i) + j)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,k0,((4 * i) + j))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,((4 * i) + j))) . (IC ) is set
(Comput (t,t9,((4 * i) + j))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + j))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,((4 * i) + j))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + j))) . (dl. 1) is V11() V12() integer ext-real set
(4 * i) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (t,t9,((4 * i) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (t,t9,((4 * i) + 1))) . (dl. 0) is V11() V12() integer ext-real set
Comput (P,k0,((4 * i) + 1)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P,k0,((4 * i) + 1))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,((4 * i) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 1))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (t,t9,((4 * i) + 1))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 1))) . (dl. 1) is V11() V12() integer ext-real set
((4 * i) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
(4 * i) + (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
(4 * i) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
((4 * i) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
(4 * i) + (2 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
IC (Comput (P,k0,((4 * i) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,((4 * i) + 1))) . (IC ) is set
Comput (P,k0,((4 * i) + 2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,k0,((4 * i) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,((4 * i) + 2))) . (IC ) is set
(4 * i) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (P,k0,((4 * i) + 3)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,k0,((4 * i) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,((4 * i) + 3))) . (IC ) is set
IC (Comput (t,t9,((4 * i) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,((4 * i) + 1))) . (IC ) is set
Comput (t,t9,((4 * i) + 2)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (t,t9,((4 * i) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 2))) . (dl. 2) is V11() V12() integer ext-real set
(Comput (t,t9,((4 * i) + 2))) . (dl. 1) is V11() V12() integer ext-real set
((Comput (t,t9,((4 * i) + 1))) . (dl. 0)) mod ((Comput (t,t9,((4 * i) + 1))) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 2))) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (t,t9,((4 * i) + 2))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,((4 * i) + 2))) . (IC ) is set
Comput (t,t9,((4 * i) + 3)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (t,t9,((4 * i) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,((4 * i) + 3))) . (IC ) is set
(Comput (t,t9,((4 * i) + 2))) . (dl. 0) is V11() V12() integer ext-real set
((Comput (t,t9,((4 * i) + 1))) . (dl. 0)) div ((Comput (t,t9,((4 * i) + 1))) . (dl. 1)) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 2))) . (dl. 0) is V11() V12() integer ext-real set
((4 * i) + 3) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
(4 * i) + (3 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
(Comput (t,t9,((4 * i) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 3))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,((4 * i) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 3))) . (dl. 1) is V11() V12() integer ext-real set
(4 * i) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (t,t9,((4 * i) + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (t,t9,((4 * i) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,((4 * i) + 4))) . (IC ) is set
Comput (P,k0,((4 * i) + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,k0,((4 * i) + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,((4 * i) + 4))) . (IC ) is set
(Comput (t,t9,((4 * i) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 4))) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,((4 * i) + 4))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,((4 * i) + 4))) . (dl. 1) is V11() V12() integer ext-real set
(Comput (t,t9,0)) . (IC ) is set
IC t9 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
t9 . (IC ) is set
IC k0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
k0 . (IC ) is set
(Comput (P,k0,0)) . (IC ) is set
IC (Comput (t,t9,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
IC (Comput (P,k0,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,0)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (P,k0,0)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,0)) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,0)) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (t,t9,k)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (t,t9,k)) . (IC ) is set
IC (Comput (P,k0,k)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,k0,k)) . (IC ) is set
(Comput (t,t9,k)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (P,k0,k)) . (dl. 0) is V11() V12() integer ext-real set
(Comput (t,t9,k)) . (dl. 1) is V11() V12() integer ext-real set
(Comput (P,k0,k)) . (dl. 1) is V11() V12() integer ext-real set
() . d is set
Result ((),((Start-At (0,SCM)) +* d)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible finite set
t is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
P is Relation-like NAT -defined the InstructionsF of SCM -valued Function-like total set
Comput (P,t,4) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
t . (dl. 1) is V11() V12() integer ext-real set
t . (dl. 0) is V11() V12() integer ext-real set
k0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,t,k0) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,t,k0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,t,k0)) . (IC ) is set
i1 mod i2 is V11() V12() integer ext-real set
i19 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i29 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i19 mod i29 is V11() V12() integer ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,t,(4 * (0 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (P,t,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Comput (P,t,4)) . (dl. 1) is V11() V12() integer ext-real set
(t . (dl. 0)) mod (t . (dl. 1)) is V11() V12() integer ext-real set
IC (Comput (P,t,4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,t,4)) . (IC ) is set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
4 * (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,t,(4 * (0 + 1))) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding finite finite-yielding V32() ext-real non positive non negative Element of NAT
Comput (P,t,(4 * 0)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
i1 mod i2 is V11() V12() integer ext-real set
i19 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i29 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
i19 mod i29 is V11() V12() integer ext-real set
(Comput (P,t,4)) . (dl. 1) is V11() V12() integer ext-real set
IC (Comput (P,t,4)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,t,4)) . (IC ) is set
(Comput (P,t,4)) . (dl. 0) is V11() V12() integer ext-real set
k0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,(Comput (P,t,4)),k0) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,(Comput (P,t,4)),k0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,(Comput (P,t,4)),k0)) . (IC ) is set
k0 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V64() ext-real positive non negative Element of NAT
Comput (P,t,(k0 + 4)) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
IC (Comput (P,t,(k0 + 4))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,t,(k0 + 4))) . (IC ) is set
Result (T,t) is Relation-like the carrier of SCM -defined Function-like K286(2,SCM) -compatible total set
(Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) is Relation-like dom ((Start-At (0,SCM)) +* d) -defined the carrier of SCM -defined finite set
dom (Result (T,t)) is set
d . (dl. 0) is set
d . (dl. 1) is set
t . (dl. 1) is V11() V12() integer ext-real set
t . (dl. 0) is V11() V12() integer ext-real set
(Result (T,t)) . (dl. 0) is V11() V12() integer ext-real set
i1 gcd i2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(dl. 0) .--> (i1 gcd i2) is V2() Relation-like the carrier of SCM -defined {(dl. 0)} -defined Function-like one-to-one K286(2,SCM) -compatible finite set
{(dl. 0)} --> (i1 gcd i2) is non empty Relation-like {(dl. 0)} -defined {(i1 gcd i2)} -valued Function-like constant finite total V40({(dl. 0)},{(i1 gcd i2)}) Element of K6(K7({(dl. 0)},{(i1 gcd i2)}))
{(i1 gcd i2)} is non empty finite set
K7({(dl. 0)},{(i1 gcd i2)}) is Relation-like finite set
K6(K7({(dl. 0)},{(i1 gcd i2)})) is finite V32() set
dom ((dl. 0) .--> (i1 gcd i2)) is V2() finite set